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

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

Proof of Theorem ad3antlr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantl 473 . 2 ((𝜒𝜑) → 𝜓)
32ad2antrr 717 1 ((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  ad4antlrOLD  727  simpllr  793  disjxiun  4806  tfrlem1  7676  oaass  7846  undom  8255  acndom2  9128  infxp  9290  isf32lem2  9429  ttukeylem3  9586  gchina  9774  r1limwun  9811  difreicc  12511  ssfzo12bi  12771  flflp1  12816  hasheqf1oi  13344  ccatcl  13545  cshwidxmodr  13834  wwlktovf1  13989  o1of2  14630  rlimsqzlem  14666  lcmgcdlem  15602  isprm5  15700  ramval  15993  mreexexlem4d  16575  acsfn  16587  gsumpropd2lem  17541  gasubg  18000  psgndiflemB  20219  psgndiflemA  20220  mdetf  20678  cpmatacl  20800  cpmatinvcl  20801  mat2pmatf1  20813  mp2pm2mplem4  20893  chfacffsupp  20940  restcld  21256  cnpnei  21348  iscncl  21353  cncls  21358  cnntr  21359  1stcfb  21528  2ndcdisj  21539  txlly  21719  fbflim  22059  fclsbas  22104  nmoi  22811  fgcfil  23348  equivcau  23377  cmetcusp  23431  itg2cnlem1  23819  iblss  23862  lgsqr  25367  lgsqrmodndvds  25369  axcontlem2  26136  nbuhgr  26518  nbusgrvtxm1  26560  2pthon3v  27146  clwwisshclwwslem  27220  wwlksext2clwwlk  27270  wwlksext2clwwlkOLD  27271  2pthfrgr  27522  vdgn1frgrv2  27534  frgrwopreg  27561  numclwlk2lem2f1o  27622  numclwlk2lem2f1oOLD  27629  blocnilem  28050  mdslmd3i  29582  foresf1o  29727  fgreu  29855  resf1o  29889  omndmul2  30094  psgnfzto1st  30237  fimaproj  30282  locfinreflem  30289  cmpcref  30299  pstmxmet  30322  lmdvg  30381  carsgclctunlem3  30764  oddpwdc  30798  sgnmul  30987  signstres  31035  tgoldbachgtd  31123  cvmlift2lem12  31676  mrsubff  31789  slerec  32299  elicc3  32687  nn0prpwlem  32692  neibastop2  32731  neibastop3  32732  ltflcei  33753  matunitlindflem2  33762  poimirlem4  33769  poimirlem13  33778  poimirlem14  33779  poimirlem26  33791  poimirlem27  33792  poimirlem28  33793  poimirlem29  33794  poimirlem31  33796  heicant  33800  mblfinlem2  33803  mblfinlem3  33804  mblfinlem4  33805  ismblfin  33806  itg2addnclem  33816  itg2addnclem2  33817  itg2addnclem3  33818  itg2addnc  33819  itg2gt0cn  33820  ftc1cnnc  33839  ftc1anclem5  33844  ftc1anclem6  33845  ftc1anclem7  33846  ftc1anclem8  33847  ftc1anc  33848  nnubfi  33900  nninfnub  33901  linepsubN  35640  lhpmatb  35919  cdlemf2  36450  diaglbN  36943  diaintclN  36946  dibglbN  37054  dibintclN  37055  dihlsscpre  37122  dihglblem5aN  37180  dihglblem2aN  37181  dih1dimatlem  37217  diophren  37987  irrapxlem2  37997  irrapxlem4  37999  wepwsolem  38221  prmunb2  39116  cvgdvgrat  39118  fiiuncl  39817  infleinflem2  40157  supxrunb3  40192  supminfxr  40263  limsuppnflem  40512  limsupmnflem  40522  limsupre3lem  40534  dfxlim2v  40643  icccncfext  40670  ioodvbdlimc1lem1  40716  iblcncfioo  40763  wallispilem3  40853  fourierdlem12  40905  fourierdlem34  40927  fourierdlem50  40942  fourierdlem51  40943  fourierdlem65  40957  fourierdlem77  40969  meaiuninc3v  41270  hoicvr  41334  hspdifhsp  41402  smflimlem4  41554  iccpartigtl  42025  iccpartgt  42029  fargshiftfva  42045  sfprmdvdsmersenne  42128  opoeALTV  42202  opeoALTV  42203  nnsum4primeseven  42296  nnsum4primesevenALTV  42297  issubmgm2  42391  uzlidlring  42530  2zrngmmgm  42547  cznrng  42556  ply1mulgsumlem2  42776  snlindsntor  42861  elbigo2  42947  nn0sumshdiglemA  43014
  Copyright terms: Public domain W3C validator