MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad3antrrr Structured version   Visualization version   GIF version

Theorem ad3antrrr 766
Description: Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad3antrrr ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem ad3antrrr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 480 . 2 ((𝜑𝜒) → 𝜓)
32ad2antrr 762 1 ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  ad4antr  769  ad4antrOLD  770  ad4antlr  771  simplll  813  ad5ant12  1331  fsnex  6578  oaabs  7769  oaabs2  7770  omabs  7772  undom  8089  sbthlem8  8118  findcard3  8244  cantnfle  8606  cantnfp1  8616  cantnflem1c  8622  sornom  9137  enfin2i  9181  ttukeylem6  9374  fpwwe2lem13  9502  fpwwe2  9503  winalim2  9556  wuncval2  9607  negf1o  10498  xlemul1a  12156  difreicc  12342  flflp1  12648  faclbnd  13117  swrdswrd  13506  swrdccatin12lem3  13536  swrdccat3blem  13541  ello12  14291  lo1bdd2  14299  elo12  14302  rlimclim1  14320  rlimcld2  14353  o1co  14361  o1of2  14387  o1rlimmul  14393  rlimsqzlem  14423  isercoll  14442  o1fsum  14589  supcvg  14632  dvds2ln  15061  lcmgcdlem  15366  cncongr2  15429  isprm5  15466  pcadd  15640  vdwlem2  15733  vdwlem11  15742  sbcie3s  15964  prdsval  16162  mreexexlem4d  16354  isacs2  16361  catcocl  16393  catass  16394  subccocl  16552  fullsubc  16557  funcco  16578  funcpropd  16607  fullpropd  16627  ffthiso  16636  isnat  16654  natpropd  16683  fucpropd  16684  xpcval  16864  evlf2  16905  curfpropd  16920  curfuncf  16925  uncfcurf  16926  curf2ndf  16934  hofcl  16946  hofpropd  16954  yonffthlem  16969  isacs3lem  17213  acsfiindd  17224  gsumpropd2lem  17320  resmhm2b  17408  mhmid  17583  mhmmnd  17584  ghmgrp  17586  conjnmzb  17742  pgpfi  18066  sylow3lem2  18089  efgredlem  18206  frgpnabllem1  18322  dprdfcntz  18460  ablfac1b  18515  pgpfac1lem3  18522  pgpfac1lem5  18524  pgpfaclem3  18528  ringinvnzdiv  18639  islmhm2  19086  lspsneleq  19163  psrval  19410  psrass1  19453  resspsrmul  19465  mplbas2  19518  coe1tmmul  19695  gsummoncoe1  19722  znunit  19960  psgndiflemB  19994  uvcff  20178  uvcf1  20179  lindfmm  20214  dmatsubcl  20352  scmatscm  20367  smatvscl  20378  marrepval  20416  mdetdiaglem  20452  mdetunilem8  20473  mdetunilem9  20474  pmatcoe1fsupp  20554  decpmatmulsumfsupp  20626  pmatcollpw2lem  20630  mp2pm2mplem4  20662  pm2mpmhmlem1  20671  pm2mpmhmlem2  20672  pm2mp  20678  fvmptnn04if  20702  cpmadugsumfi  20730  cpmidg2sum  20733  cpmadumatpoly  20736  cayhamlem4  20741  neiptoptop  20983  neitr  21032  ordtrest2lem  21055  cnpnei  21116  iscncl  21121  cncls  21126  cnntr  21127  cncnp  21132  lmcnp  21156  isreg2  21229  hauscmplem  21257  cmpfi  21259  1stcfb  21296  1stcrest  21304  2ndcctbss  21306  2ndcomap  21309  islly2  21335  cldllycmp  21346  lly1stc  21347  locfincmp  21377  llycmpkgen2  21401  1stckgenlem  21404  kgencn2  21408  kgencn3  21409  ptbasfi  21432  ptpjopn  21463  txdis1cn  21486  txlly  21487  txnlly  21488  txtube  21491  txcmplem2  21493  tx1stc  21501  txkgen  21503  xkopt  21506  xkoco2cn  21509  xkococnlem  21510  xkococn  21511  xkoinjcn  21538  tgqtop  21563  regr1lem  21590  kqreglem1  21592  nrmhmph  21645  rnelfmlem  21803  rnelfm  21804  fmfnfmlem4  21808  fmfnfm  21809  ufldom  21813  flimopn  21826  hauspwpwf1  21838  fclsopn  21865  fclsnei  21870  fclsrest  21875  alexsublem  21895  alexsubALTlem3  21900  ptcmplem2  21904  ptcmplem3  21905  cnextfun  21915  cnextcn  21918  symgtgp  21952  tgpt0  21969  qustgpopn  21970  tsmsxplem1  22003  trust  22080  utopsnneiplem  22098  utop3cls  22102  utopreg  22103  isucn2  22130  cstucnd  22135  ucncn  22136  fmucnd  22143  cfilufg  22144  neipcfilu  22147  met2ndci  22374  prdsxmslem2  22381  metcnp3  22392  metustid  22406  metustexhalf  22408  metust  22410  psmetutop  22419  nmoleub  22582  reconnlem2  22677  xrge0tsms  22684  cncfco  22757  lebnumlem3  22809  lebnum  22810  nmoleub2lem2  22962  nmoleub3  22965  iscfil2  23110  iscau4  23123  iscmet3lem2  23136  equivcfil  23143  equivcau  23144  caubl  23152  rrxdstprj1  23238  ovolshftlem2  23324  ovolicc2lem4  23334  uniioombl  23403  i1fmulclem  23514  mbfi1fseqlem6  23532  itg2const2  23553  itg2split  23561  ellimc2  23686  ellimc3  23688  limcflf  23690  dvmptfsum  23783  dvferm1  23793  dvferm2  23795  dvlip2  23803  c1lip1  23805  lhop1  23822  ftc1a  23845  ply1divex  23941  plyeq0lem  24011  plymullem1  24015  coemullem  24051  coemulc  24056  ulmshftlem  24188  ulmcaulem  24193  ulmbdd  24197  ulmcn  24198  ulmdvlem3  24201  mtestbdd  24204  pserulm  24221  pserdvlem2  24227  abelthlem8  24238  xrlimcnp  24740  jensen  24760  lgamucov  24809  logfac2  24987  dchrelbas3  25008  dchrpt  25037  gausslemma2dlem1a  25135  lgsquad3  25157  2sqb  25202  rpvmasumlem  25221  dchrisumlem1  25223  dchrisumlem3  25225  dchrmusum2  25228  dchrvmasumlem2  25232  dchrisum0flblem1  25242  dchrisum0lem1b  25249  dchrisum0lem1  25250  dchrisum0  25254  mulog2sumlem2  25269  pntlem3  25343  ostth3  25372  istrkgcb  25400  tgbtwndiff  25446  iscgrglt  25454  tgcgrxfr  25458  motcgrg  25484  lnext  25507  tgbtwnconn1  25515  tgbtwnconn3  25517  legval  25524  legtrid  25531  legso  25539  hlcgreu  25558  tglnne  25568  tglineeltr  25571  tglnne0  25580  colline  25589  tglowdim2l  25590  tglowdim2ln  25591  mirreu3  25594  mirbtwnhl  25620  krippenlem  25630  midexlem  25632  perpcom  25653  perpneq  25654  footex  25658  colperpexlem3  25669  colperpex  25670  opphllem  25672  midex  25674  oppne3  25680  opptgdim2  25682  oppnid  25683  opphllem2  25685  opphllem5  25688  opphllem6  25689  oppperpex  25690  outpasch  25692  hlpasch  25693  lnopp2hpgb  25700  hpgerlem  25702  colopp  25706  colhp  25707  lmieu  25721  lnperpex  25740  trgcopy  25741  trgcopyeulem  25742  iscgra1  25747  cgrane1  25749  cgrane2  25750  cgrane3  25751  cgrane4  25752  cgrahl1  25753  cgrahl2  25754  cgracgr  25755  cgraswap  25757  cgracom  25759  cgratr  25760  cgrabtwn  25762  cgrahl  25763  sacgr  25767  acopyeu  25770  cgrg3col4  25779  tgasa1  25784  f1otrg  25796  f1otrge  25797  axeuclidlem  25887  axcontlem2  25890  umgrvad2edg  26150  usgredg2vlem2  26163  pthdepisspth  26687  wwlksnwwlksnonOLD  26880  clwlkclwwlklem2  26966  wwlksext2clwwlkOLD  27022  clwlksf1clwwlk  27056  3cycld  27156  eupth2lems  27216  eucrctshift  27221  frgr3vlem2  27254  n4cyclfrgr  27271  clwwlkccatlem  27331  numclwlk1lem2f1  27347  numclwwlk2lem1  27356  numclwwlk2lem1OLD  27363  ubthlem3  27856  chirredlem1  29377  chirredlem3  29379  cdj1i  29420  xrge0infss  29653  omndmul2  29840  submarchi  29868  gsumle  29907  xrge0tsmsd  29913  suborng  29943  isarchiofld  29945  psgnfzto1stlem  29978  fzto1st1  29980  smatrcl  29990  1smat1  29998  submateq  30003  mdetpmtr1  30017  madjusmdetlem2  30022  fimaproj  30028  locfinreflem  30035  cmppcmp  30053  ordtrest2NEWlem  30096  ordtconnlem1  30098  lmdvg  30127  esumpcvgval  30268  esum2d  30283  sigapildsys  30353  ldgenpisyslem1  30354  fiunelros  30365  volmeas  30422  imambfm  30452  omssubadd  30490  carsggect  30508  carsgclctunlem3  30510  sgnmul  30732  signsply0  30756  signstres  30780  actfunsnf1o  30810  actfunsnrndisj  30811  reprsuc  30821  reprinfz1  30828  breprexplema  30836  breprexplemc  30838  breprexp  30839  breprexpnat  30840  circlemeth  30846  hgt750lemb  30862  tgoldbachgtd  30868  erdszelem8  31306  pconnconn  31339  cvmlift2lem12  31422  cvmlift3lem5  31431  cvmlift3lem7  31433  cvmlift3lem8  31434  mrsubrn  31536  msrval  31561  msubff1  31579  slerec  32048  btwnconn1lem13  32331  elicc3  32436  neibastop2lem  32480  unbdqndv2  32627  ltflcei  33527  lindsenlbs  33534  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem4  33543  poimirlem13  33552  poimirlem14  33553  poimirlem22  33561  poimirlem26  33565  poimirlem27  33566  heicant  33574  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  cnambfre  33588  itg2addnclem  33591  itg2addnclem2  33592  itg2gt0cn  33595  bddiblnc  33610  ftc1cnnc  33614  ftc1anclem5  33619  ftc1anclem7  33621  ftc1anc  33623  equivtotbnd  33707  isbndx  33711  ssbnd  33717  heibor1lem  33738  rrncmslem  33761  islshpat  34622  lfl1dim  34726  lfl1dim2N  34727  lkrpssN  34768  glbconN  34981  hlhgt2  34993  3dim2  35072  3dim3  35073  islln3  35114  islvol5  35183  2lplnja  35223  dalem19  35286  isline4N  35381  2polssN  35519  lhpmatb  35635  4atex  35680  trlatn0  35777  cdlemf2  36167  dialss  36652  diaglbN  36661  diaintclN  36664  dibglbN  36772  dibintclN  36773  dihlsscpre  36840  dihglblem5aN  36898  dihglblem2aN  36899  dihglblem4  36903  dihatexv  36944  dihjat1lem  37034  lcfl6  37106  mapdval2N  37236  elrfi  37574  eldioph2  37642  diophin  37653  irrapxlem2  37704  irrapxlem3  37705  irrapxlem4  37706  irrapxlem5  37707  pell1234qrne0  37734  pell1234qrreccl  37735  pell1234qrmulcl  37736  pell14qrgt0  37740  pell14qrdich  37750  pell1qrge1  37751  pellfundex  37767  congabseq  37858  jm2.27b  37890  jm2.27  37892  fnwe2lem2  37938  kelac1  37950  lnrfg  38006  hbt  38017  cntzsdrg  38089  rfovcnvf1od  38615  ntrneiiso  38706  ntrneikb  38709  ntrneixb  38710  ntrneik3  38711  ntrneix3  38712  ntrneik13  38713  ntrneix13  38714  cvgdvgrat  38829  binomcxplemnotnn0  38872  sineq0ALT  39487  disjf1  39683  supxrgere  39862  supxrgelem  39866  supxrge  39867  suplesup  39868  xralrple2  39883  infxr  39896  infleinflem2  39900  infleinf  39901  uzub  39971  mccl  40148  limcrecl  40179  lptioo2  40181  lptioo1  40182  lptre2pt  40190  addlimc  40198  limsupmnflem  40270  climxrre  40300  liminflimsupclim  40357  climxlim2lem  40389  icccncfext  40418  cncfiooicclem1  40424  cncfiooiccre  40426  dvbdfbdioolem2  40462  ioodvbdlimc1lem1  40464  dvnxpaek  40475  dvmptfprodlem  40477  dvmptfprod  40478  dvnprodlem3  40481  itgioocnicc  40511  itgspltprt  40513  stoweidlem31  40566  fourierdlem39  40681  fourierdlem42  40684  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem51  40692  fourierdlem64  40705  fourierdlem65  40706  fourierdlem74  40715  fourierdlem75  40716  fourierdlem81  40722  fourierdlem82  40723  fourierdlem101  40742  etransclem23  40792  etransclem27  40796  etransclem32  40801  etransclem33  40802  etransclem35  40804  etransclem38  40807  sge0tsms  40915  sge0cl  40916  sge0f1o  40917  sge0split  40944  sge0rpcpnf  40956  sge0seq  40981  nnfoctbdjlem  40990  iundjiun  40995  meaiuninc3v  41019  meaiininclem  41021  omeiunltfirp  41054  carageniuncllem2  41057  carageniuncl  41058  hoidmv1lelem1  41126  hoidmvlelem3  41132  hoidmvlelem5  41134  hoidmvle  41135  hoiqssbllem3  41159  iunhoiioolem  41210  pimdecfgtioo  41248  pimincfltioo  41249  preimageiingt  41251  preimaleiinlt  41252  smflimlem4  41303  iccpartigtl  41684  iccpartgt  41688  proththd  41856  sbgoldbst  41991  bgoldbtbndlem4  42021  sprsymrelf1lem  42066  resmgmhm2b  42125  2zrngmmgm  42271  cznrng  42280  rnghmsubcsetclem2  42301  rhmsubcsetclem2  42347  srhmsubc  42401  rhmsubclem4  42414  srhmsubcALTV  42419  rhmsubcALTVlem4  42432  lincsum  42543  lcoss  42550  snlindsntor  42585  islindeps2  42597
  Copyright terms: Public domain W3C validator