Theorem ad3antlr 730

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 725	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  775  disjxiun  5139  fimaproj  8134  tfrlem1  8390  oaass  8575  undomOLD  9076  acndom2  10069  infxp  10230  isf32lem2  10369  ttukeylem3  10526  gchina  10714  r1limwun  10751  difreicc  13485  ssfzo12bi  13751  flflp1  13796  hasheqf1oi  14334  ccatcl  14548  cshwidxmodr  14778  wwlktovf1  14932  o1of2  15581  rlimsqzlem  15619  lcmgcdlem  16568  isprm5  16669  ramval  16968  mreexexlem4d  17618  acsfn  17630  gsumpropd2lem  18630  issubmgm2  18654  gasubg  19244  psgndiflemB  21519  psgndiflemA  21520  psrass1  21894  mdetf  22484  cpmatacl  22605  cpmatinvcl  22606  mat2pmatf1  22618  mp2pm2mplem4  22698  chfacffsupp  22745  restcld  23063  cnpnei  23155  iscncl  23160  cncls  23165  cnntr  23166  1stcfb  23336  2ndcdisj  23347  txlly  23527  fbflim  23867  fclsbas  23912  nmoi  24632  mpomulcn  24772  fgcfil  25186  equivcau  25215  cmetcusp  25269  itg2cnlem1  25678  iblss  25721  lgsqr  27271  lgsqrmodndvds  27273  noetainflem4  27660  slerec  27739  remulscllem2  28216  axcontlem2  28763  nbuhgr  29143  nbusgrvtxm1  29179  2pthon3v  29741  clwwisshclwwslem  29811  wwlksext2clwwlk  29854  2pthfrgr  30081  vdgn1frgrv2  30093  frgrwopreg  30120  numclwlk2lem2f1o  30176  blocnilem  30601  mdslmd3i  32129  foresf1o  32286  2ndresdju  32418  fgreu  32441  fdifsuppconst  32453  resf1o  32496  omndmul2  32770  psgnfzto1st  32804  isdrng4  32932  nsgqusf1olem3  33065  elrspunidl  33079  elrspunsn  33080  qsidomlem1  33104  lbsdiflsp0  33256  evls1fldgencl  33290  ist0cld  33370  locfinreflem  33377  cmpcref  33387  zarclsun  33407  pstmxmet  33434  lmdvg  33490  carsgclctunlem3  33876  oddpwdc  33910  sgnmul  34098  signstres  34143  tgoldbachgtd  34230  cvmlift2lem12  34860  satfdmlem  34914  satffunlem2lem1  34950  mrsubff  35058  elicc3  35737  nn0prpwlem  35742  neibastop2  35781  neibastop3  35782  bj-prmoore  36530  ltflcei  37016  matunitlindflem2  37025  poimirlem4  37032  poimirlem13  37041  poimirlem14  37042  poimirlem26  37054  poimirlem27  37055  poimirlem28  37056  poimirlem29  37057  poimirlem31  37059  heicant  37063  mblfinlem2  37066  mblfinlem3  37067  mblfinlem4  37068  ismblfin  37069  itg2addnclem  37079  itg2addnclem2  37080  itg2addnclem3  37081  itg2addnc  37082  itg2gt0cn  37083  ftc1cnnc  37100  ftc1anclem5  37105  ftc1anclem6  37106  ftc1anclem7  37107  ftc1anclem8  37108  ftc1anc  37109  nnubfi  37158  nninfnub  37159  linepsubN  39162  lhpmatb  39441  cdlemf2  39972  diaglbN  40465  diaintclN  40468  dibglbN  40576  dibintclN  40577  dihlsscpre  40644  dihglblem5aN  40702  dihglblem2aN  40703  dih1dimatlem  40739  sticksstones12a  41561  fsuppind  41745  diophren  42155  irrapxlem2  42165  irrapxlem4  42167  wepwsolem  42388  omlimcl2  42593  tfsconcatfv  42693  ofoafg  42706  prmunb2  43671  cvgdvgrat  43673  fiiuncl  44352  infleinflem2  44676  supxrunb3  44704  supminfxr  44769  limsuppnflem  45021  limsupmnflem  45031  limsupre3lem  45043  dfxlim2v  45158  icccncfext  45198  ioodvbdlimc1lem1  45242  iblcncfioo  45289  wallispilem3  45378  fourierdlem12  45430  fourierdlem34  45452  fourierdlem50  45467  fourierdlem51  45468  fourierdlem65  45482  fourierdlem77  45494  meaiuninc3v  45795  hoicvr  45859  hspdifhsp  45927  smflimlem4  46085  iccpartigtl  46686  iccpartgt  46690  fargshiftfva  46706  sfprmdvdsmersenne  46866  opoeALTV  46946  opeoALTV  46947  nnsum4primeseven  47063  nnsum4primesevenALTV  47064  isuspgrimlem  47095  gricushgr  47106  uzlidlring  47220  2zrngmmgm  47237  cznrng  47246  ply1mulgsumlem2  47378  snlindsntor  47462  elbigo2  47548  nn0sumshdiglemA  47615