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 485	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad2antrr 725	1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  simpllr  775  disjxiun  5027  fimaproj  7812  tfrlem1  7995  oaass  8170  undom  8588  acndom2  9465  infxp  9626  isf32lem2  9765  ttukeylem3  9922  gchina  10110  r1limwun  10147  difreicc  12862  ssfzo12bi  13127  flflp1  13172  hasheqf1oi  13708  ccatcl  13917  cshwidxmodr  14157  wwlktovf1  14312  o1of2  14961  rlimsqzlem  14997  lcmgcdlem  15940  isprm5  16041  ramval  16334  mreexexlem4d  16910  acsfn  16922  gsumpropd2lem  17881  gasubg  18424  psgndiflemB  20289  psgndiflemA  20290  mdetf  21200  cpmatacl  21321  cpmatinvcl  21322  mat2pmatf1  21334  mp2pm2mplem4  21414  chfacffsupp  21461  restcld  21777  cnpnei  21869  iscncl  21874  cncls  21879  cnntr  21880  1stcfb  22050  2ndcdisj  22061  txlly  22241  fbflim  22581  fclsbas  22626  nmoi  23334  fgcfil  23875  equivcau  23904  cmetcusp  23958  itg2cnlem1  24365  iblss  24408  lgsqr  25935  lgsqrmodndvds  25937  axcontlem2  26759  nbuhgr  27133  nbusgrvtxm1  27169  2pthon3v  27729  clwwisshclwwslem  27799  wwlksext2clwwlk  27842  2pthfrgr  28069  vdgn1frgrv2  28081  frgrwopreg  28108  numclwlk2lem2f1o  28164  blocnilem  28587  mdslmd3i  30115  foresf1o  30273  2ndresdju  30411  fgreu  30435  fdifsuppconst  30449  resf1o  30492  omndmul2  30763  psgnfzto1st  30797  elrspunidl  31014  qsidomlem1  31036  lbsdiflsp0  31110  ist0cld  31186  locfinreflem  31193  cmpcref  31203  zarclsun  31223  pstmxmet  31250  lmdvg  31306  carsgclctunlem3  31688  oddpwdc  31722  sgnmul  31910  signstres  31955  tgoldbachgtd  32043  cvmlift2lem12  32674  satfdmlem  32728  satffunlem2lem1  32764  mrsubff  32872  slerec  33390  elicc3  33778  nn0prpwlem  33783  neibastop2  33822  neibastop3  33823  bj-prmoore  34530  ltflcei  35045  matunitlindflem2  35054  poimirlem4  35061  poimirlem13  35070  poimirlem14  35071  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  poimirlem29  35086  poimirlem31  35088  heicant  35092  mblfinlem2  35095  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  itg2addnclem  35108  itg2addnclem2  35109  itg2addnclem3  35110  itg2addnc  35111  itg2gt0cn  35112  ftc1cnnc  35129  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  nnubfi  35188  nninfnub  35189  linepsubN  37048  lhpmatb  37327  cdlemf2  37858  diaglbN  38351  diaintclN  38354  dibglbN  38462  dibintclN  38463  dihlsscpre  38530  dihglblem5aN  38588  dihglblem2aN  38589  dih1dimatlem  38625  fsuppind  39456  diophren  39754  irrapxlem2  39764  irrapxlem4  39766  wepwsolem  39986  prmunb2  41015  cvgdvgrat  41017  fiiuncl  41699  infleinflem2  42003  supxrunb3  42036  supminfxr  42103  limsuppnflem  42352  limsupmnflem  42362  limsupre3lem  42374  dfxlim2v  42489  icccncfext  42529  ioodvbdlimc1lem1  42573  iblcncfioo  42620  wallispilem3  42709  fourierdlem12  42761  fourierdlem34  42783  fourierdlem50  42798  fourierdlem51  42799  fourierdlem65  42813  fourierdlem77  42825  meaiuninc3v  43123  hoicvr  43187  hspdifhsp  43255  smflimlem4  43407  iccpartigtl  43940  iccpartgt  43944  fargshiftfva  43960  sfprmdvdsmersenne  44121  opoeALTV  44201  opeoALTV  44202  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  isomushgr  44344  isomuspgr  44352  issubmgm2  44410  uzlidlring  44553  2zrngmmgm  44570  cznrng  44579  ply1mulgsumlem2  44795  snlindsntor  44880  elbigo2  44966  nn0sumshdiglemA  45033