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  5083  fimaproj  8076  tfrlem1  8306  oaass  8487  acndom2  9965  infxp  10125  isf32lem2  10265  ttukeylem3  10422  gchina  10611  r1limwun  10648  difreicc  13426  ssfzo12bi  13705  flflp1  13755  hasheqf1oi  14302  ccatcl  14525  cshwidxmodr  14755  wwlktovf1  14908  o1of2  15564  rlimsqzlem  15600  lcmgcdlem  16564  isprm5  16666  ramval  16968  mreexexlem4d  17602  acsfn  17614  chnso  18579  gsumpropd2lem  18636  issubmgm2  18660  gasubg  19266  omndmul2  20097  psgndiflemB  21588  psgndiflemA  21589  psrass1  21951  mhpmulcl  22124  mdetf  22569  cpmatacl  22690  cpmatinvcl  22691  mat2pmatf1  22703  mp2pm2mplem4  22783  chfacffsupp  22830  restcld  23146  cnpnei  23238  iscncl  23243  cncls  23248  cnntr  23249  1stcfb  23419  2ndcdisj  23430  txlly  23610  fbflim  23950  fclsbas  23995  nmoi  24702  mpomulcn  24843  fgcfil  25247  equivcau  25276  cmetcusp  25330  itg2cnlem1  25737  iblss  25781  lgsqr  27333  lgsqrmodndvds  27335  noetainflem4  27723  lesrec  27810  remulscllem2  28512  axcontlem2  29053  nbuhgr  29431  nbusgrvtxm1  29467  2pthon3v  30031  clwwisshclwwslem  30104  wwlksext2clwwlk  30147  2pthfrgr  30374  vdgn1frgrv2  30386  frgrwopreg  30413  numclwlk2lem2f1o  30469  blocnilem  30895  mdslmd3i  32423  foresf1o  32594  2ndresdju  32742  fgreu  32764  fdifsuppconst  32782  resf1o  32823  sgnmul  32928  psgnfzto1st  33186  elrgspnsubrunlem1  33328  isdrng4  33376  nsgqusf1olem3  33495  elrspunidl  33508  elrspunsn  33509  qsidomlem1  33532  1arithidom  33617  dfufd2lem  33629  mplvrpmga  33709  lbsdiflsp0  33791  evls1fldgencl  33835  cos9thpiminplylem2  33948  ist0cld  33998  locfinreflem  34005  cmpcref  34015  zarclsun  34035  pstmxmet  34062  lmdvg  34118  carsgclctunlem3  34485  oddpwdc  34519  signstres  34740  tgoldbachgtd  34827  cvmlift2lem12  35517  satfdmlem  35571  satffunlem2lem1  35607  mrsubff  35715  elicc3  36520  nn0prpwlem  36525  neibastop2  36564  neibastop3  36565  bj-prmoore  37440  ltflcei  37940  matunitlindflem2  37949  poimirlem4  37956  poimirlem13  37965  poimirlem14  37966  poimirlem26  37978  poimirlem27  37979  poimirlem28  37980  poimirlem29  37981  poimirlem31  37983  heicant  37987  mblfinlem2  37990  mblfinlem3  37991  mblfinlem4  37992  ismblfin  37993  itg2addnclem  38003  itg2addnclem2  38004  itg2addnclem3  38005  itg2addnc  38006  itg2gt0cn  38007  ftc1cnnc  38024  ftc1anclem5  38029  ftc1anclem6  38030  ftc1anclem7  38031  ftc1anclem8  38032  ftc1anc  38033  nnubfi  38082  nninfnub  38083  linepsubN  40209  lhpmatb  40488  cdlemf2  41019  diaglbN  41512  diaintclN  41515  dibglbN  41623  dibintclN  41624  dihlsscpre  41691  dihglblem5aN  41749  dihglblem2aN  41750  dih1dimatlem  41786  sticksstones12a  42607  fsuppind  43034  diophren  43256  irrapxlem2  43266  irrapxlem4  43268  wepwsolem  43485  omlimcl2  43685  tfsconcatfv  43784  ofoafg  43797  prmunb2  44753  cvgdvgrat  44755  fiiuncl  45511  infleinflem2  45815  supxrunb3  45843  supminfxr  45907  limsuppnflem  46153  limsupmnflem  46163  limsupre3lem  46175  dfxlim2v  46290  icccncfext  46330  ioodvbdlimc1lem1  46374  iblcncfioo  46421  wallispilem3  46510  fourierdlem12  46562  fourierdlem34  46584  fourierdlem50  46599  fourierdlem51  46600  fourierdlem65  46614  fourierdlem77  46626  meaiuninc3v  46927  hspdifhsp  47059  smflimlem4  47217  iccpartigtl  47880  iccpartgt  47884  fargshiftfva  47900  sfprmdvdsmersenne  48063  opoeALTV  48156  opeoALTV  48157  nnsum4primeseven  48273  nnsum4primesevenALTV  48274  uhgrimedgi  48363  isuspgrimlem  48368  gricushgr  48390  isubgr3stgrlem7  48445  uspgrlimlem4  48464  gpgedgvtx1  48535  pgn4cyclex  48599  uzlidlring  48708  2zrngmmgm  48725  cznrng  48734  ply1mulgsumlem2  48860  snlindsntor  48944  elbigo2  49025  nn0sumshdiglemA  49092  precofvalALT  49840