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

Theorem ad3antlr 763
Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad3antlr ((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem ad3antlr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21ad2antlr 759 . 2 (((𝜒𝜑) ∧ 𝜃) → 𝜓)
32adantr 480 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 196  df-an 385
This theorem is referenced by:  ad4antlr  765  disjxiun  4579  tfrlem1  7359  oaass  7528  undom  7933  acndom2  8760  infxp  8920  isf32lem2  9059  ttukeylem3  9216  gchina  9400  r1limwun  9437  difreicc  12175  ssfzo12bi  12429  flflp1  12470  hasheqf1oi  13002  ccatcl  13212  cshwidxmodr  13401  wwlktovf1  13548  o1of2  14191  rlimsqzlem  14227  lcmgcdlem  15157  isprm5  15257  ramval  15550  mreexexlem4d  16130  acsfn  16143  gsumpropd2lem  17096  gasubg  17558  psgndiflemB  19765  psgndiflemA  19766  mdetf  20220  cpmatacl  20340  cpmatinvcl  20341  mat2pmatf1  20353  mp2pm2mplem4  20433  chfacffsupp  20480  restcld  20786  cnpnei  20878  iscncl  20883  cncls  20888  cnntr  20889  1stcfb  21058  2ndcdisj  21069  txlly  21249  fbflim  21590  fclsbas  21635  nmoi  22342  fgcfil  22877  equivcau  22906  cmetcusp  22958  itg2cnlem1  23334  iblss  23377  lgsqr  24876  lgsqrmodndvds  24878  axcontlem2  25645  usgra2wlkspth  26149  fargshiftfva  26167  constr3trllem2  26179  wlkiswwlk1  26218  wwlkext2clwwlk  26331  clwwisshclwwlem  26334  eupatrl  26495  frgra2v  26526  vdn1frgrav2  26552  vdgn1frgrav2  26553  frgrawopreg  26576  2spotiundisj  26589  usgreg2spot  26594  numclwlk1lem2f1  26621  numclwlk2lem2f1o  26632  blocnilem  27043  mdslmd3i  28575  foresf1o  28727  fgreu  28854  resf1o  28893  omndmul2  29043  psgnfzto1st  29186  fimaproj  29228  locfinreflem  29235  cmpcref  29245  pstmxmet  29268  lmdvg  29327  carsgclctunlem3  29709  oddpwdc  29743  sgnmul  29931  signstres  29978  cvmlift2lem12  30550  mrsubff  30663  elicc3  31481  nn0prpwlem  31487  neibastop2  31526  neibastop3  31527  ltflcei  32567  matunitlindflem2  32576  poimirlem4  32583  poimirlem13  32592  poimirlem14  32593  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem29  32608  poimirlem31  32610  heicant  32614  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  itg2addnclem  32631  itg2addnclem2  32632  itg2addnclem3  32633  itg2addnc  32634  itg2gt0cn  32635  ftc1cnnc  32654  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  nnubfi  32716  nninfnub  32717  linepsubN  34056  lhpmatb  34335  cdlemf2  34868  diaglbN  35362  diaintclN  35365  dibglbN  35473  dibintclN  35474  dihlsscpre  35541  dihglblem5aN  35599  dihglblem2aN  35600  dih1dimatlem  35636  diophren  36395  irrapxlem2  36405  irrapxlem4  36407  wepwsolem  36630  prmunb2  37532  cvgdvgrat  37534  fiiuncl  38259  infleinflem2  38528  icccncfext  38773  ioodvbdlimc1lem1  38821  iblcncfioo  38870  wallispilem3  38960  fourierdlem12  39012  fourierdlem34  39034  fourierdlem50  39049  fourierdlem51  39050  fourierdlem65  39064  fourierdlem77  39076  hoicvr  39438  hspdifhsp  39506  smflimlem4  39660  iccpartigtl  39961  iccpartgt  39965  sfprmdvdsmersenne  40058  opoeALTV  40132  opeoALTV  40133  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  nbuhgr  40565  nbusgrvtxm1  40607  2pthon3v-av  41150  wwlksext2clwwlk  41231  clwwisshclwwslem  41234  2pthfrgr  41454  vdgn1frgrv2  41466  frgrwopreg  41486  av-numclwlk1lem2f1  41524  av-numclwlk2lem2f1o  41535  issubmgm2  41580  uzlidlring  41719  2zrngmmgm  41736  cznrng  41747  ply1mulgsumlem2  41969  snlindsntor  42054  elbigo2  42144  nn0sumshdiglemA  42211
  Copyright terms: Public domain W3C validator