Theorem ad3antlr 732

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 727	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 207  df-an 396

This theorem is referenced by:  simpllr  776  disjxiun  5096  fimaproj  8079  tfrlem1  8309  oaass  8490  acndom2  9968  infxp  10128  isf32lem2  10268  ttukeylem3  10425  gchina  10614  r1limwun  10651  difreicc  13404  ssfzo12bi  13681  flflp1  13731  hasheqf1oi  14278  ccatcl  14501  cshwidxmodr  14731  wwlktovf1  14884  o1of2  15540  rlimsqzlem  15576  lcmgcdlem  16537  isprm5  16638  ramval  16940  mreexexlem4d  17574  acsfn  17586  chnso  18551  gsumpropd2lem  18608  issubmgm2  18632  gasubg  19235  omndmul2  20066  psgndiflemB  21559  psgndiflemA  21560  psrass1  21923  mhpmulcl  22096  mdetf  22543  cpmatacl  22664  cpmatinvcl  22665  mat2pmatf1  22677  mp2pm2mplem4  22757  chfacffsupp  22804  restcld  23120  cnpnei  23212  iscncl  23217  cncls  23222  cnntr  23223  1stcfb  23393  2ndcdisj  23404  txlly  23584  fbflim  23924  fclsbas  23969  nmoi  24676  mpomulcn  24818  fgcfil  25231  equivcau  25260  cmetcusp  25314  itg2cnlem1  25722  iblss  25766  lgsqr  27322  lgsqrmodndvds  27324  noetainflem4  27712  slerec  27797  remulscllem2  28480  axcontlem2  29021  nbuhgr  29399  nbusgrvtxm1  29435  2pthon3v  29999  clwwisshclwwslem  30072  wwlksext2clwwlk  30115  2pthfrgr  30342  vdgn1frgrv2  30354  frgrwopreg  30381  numclwlk2lem2f1o  30437  blocnilem  30862  mdslmd3i  32390  foresf1o  32561  2ndresdju  32709  fgreu  32731  fdifsuppconst  32749  resf1o  32790  sgnmul  32897  psgnfzto1st  33168  elrgspnsubrunlem1  33310  isdrng4  33358  nsgqusf1olem3  33477  elrspunidl  33490  elrspunsn  33491  qsidomlem1  33514  1arithidom  33599  dfufd2lem  33611  mplvrpmga  33691  lbsdiflsp0  33764  evls1fldgencl  33808  cos9thpiminplylem2  33921  ist0cld  33971  locfinreflem  33978  cmpcref  33988  zarclsun  34008  pstmxmet  34035  lmdvg  34091  carsgclctunlem3  34458  oddpwdc  34492  signstres  34713  tgoldbachgtd  34800  cvmlift2lem12  35489  satfdmlem  35543  satffunlem2lem1  35579  mrsubff  35687  elicc3  36492  nn0prpwlem  36497  neibastop2  36536  neibastop3  36537  bj-prmoore  37291  ltflcei  37780  matunitlindflem2  37789  poimirlem4  37796  poimirlem13  37805  poimirlem14  37806  poimirlem26  37818  poimirlem27  37819  poimirlem28  37820  poimirlem29  37821  poimirlem31  37823  heicant  37827  mblfinlem2  37830  mblfinlem3  37831  mblfinlem4  37832  ismblfin  37833  itg2addnclem  37843  itg2addnclem2  37844  itg2addnclem3  37845  itg2addnc  37846  itg2gt0cn  37847  ftc1cnnc  37864  ftc1anclem5  37869  ftc1anclem6  37870  ftc1anclem7  37871  ftc1anclem8  37872  ftc1anc  37873  nnubfi  37922  nninfnub  37923  linepsubN  40049  lhpmatb  40328  cdlemf2  40859  diaglbN  41352  diaintclN  41355  dibglbN  41463  dibintclN  41464  dihlsscpre  41531  dihglblem5aN  41589  dihglblem2aN  41590  dih1dimatlem  41626  sticksstones12a  42448  fsuppind  42869  diophren  43091  irrapxlem2  43101  irrapxlem4  43103  wepwsolem  43320  omlimcl2  43520  tfsconcatfv  43619  ofoafg  43632  prmunb2  44588  cvgdvgrat  44590  fiiuncl  45346  infleinflem2  45651  supxrunb3  45679  supminfxr  45744  limsuppnflem  45990  limsupmnflem  46000  limsupre3lem  46012  dfxlim2v  46127  icccncfext  46167  ioodvbdlimc1lem1  46211  iblcncfioo  46258  wallispilem3  46347  fourierdlem12  46399  fourierdlem34  46421  fourierdlem50  46436  fourierdlem51  46437  fourierdlem65  46451  fourierdlem77  46463  meaiuninc3v  46764  hoicvr  46828  hspdifhsp  46896  smflimlem4  47054  iccpartigtl  47705  iccpartgt  47709  fargshiftfva  47725  sfprmdvdsmersenne  47885  opoeALTV  47965  opeoALTV  47966  nnsum4primeseven  48082  nnsum4primesevenALTV  48083  uhgrimedgi  48172  isuspgrimlem  48177  gricushgr  48199  isubgr3stgrlem7  48254  uspgrlimlem4  48273  gpgedgvtx1  48344  pgn4cyclex  48408  uzlidlring  48517  2zrngmmgm  48534  cznrng  48543  ply1mulgsumlem2  48669  snlindsntor  48753  elbigo2  48834  nn0sumshdiglemA  48901  precofvalALT  49649