Theorem ad3antlr 727

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

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 481	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad2antrr 722	1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  simpllr  772  disjxiun  5067  fimaproj  7947  tfrlem1  8178  oaass  8354  undom  8800  acndom2  9741  infxp  9902  isf32lem2  10041  ttukeylem3  10198  gchina  10386  r1limwun  10423  difreicc  13145  ssfzo12bi  13410  flflp1  13455  hasheqf1oi  13994  ccatcl  14205  cshwidxmodr  14445  wwlktovf1  14600  o1of2  15250  rlimsqzlem  15288  lcmgcdlem  16239  isprm5  16340  ramval  16637  mreexexlem4d  17273  acsfn  17285  gsumpropd2lem  18278  gasubg  18823  psgndiflemB  20717  psgndiflemA  20718  mdetf  21652  cpmatacl  21773  cpmatinvcl  21774  mat2pmatf1  21786  mp2pm2mplem4  21866  chfacffsupp  21913  restcld  22231  cnpnei  22323  iscncl  22328  cncls  22333  cnntr  22334  1stcfb  22504  2ndcdisj  22515  txlly  22695  fbflim  23035  fclsbas  23080  nmoi  23798  fgcfil  24340  equivcau  24369  cmetcusp  24423  itg2cnlem1  24831  iblss  24874  lgsqr  26404  lgsqrmodndvds  26406  axcontlem2  27236  nbuhgr  27613  nbusgrvtxm1  27649  2pthon3v  28209  clwwisshclwwslem  28279  wwlksext2clwwlk  28322  2pthfrgr  28549  vdgn1frgrv2  28561  frgrwopreg  28588  numclwlk2lem2f1o  28644  blocnilem  29067  mdslmd3i  30595  foresf1o  30751  2ndresdju  30887  fgreu  30911  fdifsuppconst  30925  resf1o  30967  omndmul2  31240  psgnfzto1st  31274  nsgqusf1olem3  31502  elrspunidl  31508  qsidomlem1  31530  lbsdiflsp0  31609  ist0cld  31685  locfinreflem  31692  cmpcref  31702  zarclsun  31722  pstmxmet  31749  lmdvg  31805  carsgclctunlem3  32187  oddpwdc  32221  sgnmul  32409  signstres  32454  tgoldbachgtd  32542  cvmlift2lem12  33176  satfdmlem  33230  satffunlem2lem1  33266  mrsubff  33374  noetainflem4  33870  slerec  33940  elicc3  34433  nn0prpwlem  34438  neibastop2  34477  neibastop3  34478  bj-prmoore  35213  ltflcei  35692  matunitlindflem2  35701  poimirlem4  35708  poimirlem13  35717  poimirlem14  35718  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem29  35733  poimirlem31  35735  heicant  35739  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  itg2addnclem  35755  itg2addnclem2  35756  itg2addnclem3  35757  itg2addnc  35758  itg2gt0cn  35759  ftc1cnnc  35776  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  nnubfi  35835  nninfnub  35836  linepsubN  37693  lhpmatb  37972  cdlemf2  38503  diaglbN  38996  diaintclN  38999  dibglbN  39107  dibintclN  39108  dihlsscpre  39175  dihglblem5aN  39233  dihglblem2aN  39234  dih1dimatlem  39270  sticksstones12a  40041  fsuppind  40202  diophren  40551  irrapxlem2  40561  irrapxlem4  40563  wepwsolem  40783  prmunb2  41818  cvgdvgrat  41820  fiiuncl  42502  infleinflem2  42800  supxrunb3  42829  supminfxr  42894  limsuppnflem  43141  limsupmnflem  43151  limsupre3lem  43163  dfxlim2v  43278  icccncfext  43318  ioodvbdlimc1lem1  43362  iblcncfioo  43409  wallispilem3  43498  fourierdlem12  43550  fourierdlem34  43572  fourierdlem50  43587  fourierdlem51  43588  fourierdlem65  43602  fourierdlem77  43614  meaiuninc3v  43912  hoicvr  43976  hspdifhsp  44044  smflimlem4  44196  iccpartigtl  44763  iccpartgt  44767  fargshiftfva  44783  sfprmdvdsmersenne  44943  opoeALTV  45023  opeoALTV  45024  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  isomushgr  45166  isomuspgr  45174  issubmgm2  45232  uzlidlring  45375  2zrngmmgm  45392  cznrng  45401  ply1mulgsumlem2  45616  snlindsntor  45700  elbigo2  45786  nn0sumshdiglemA  45853