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  8085  tfrlem1  8315  oaass  8496  acndom2  9976  infxp  10136  isf32lem2  10276  ttukeylem3  10433  gchina  10622  r1limwun  10659  difreicc  13437  ssfzo12bi  13716  flflp1  13766  hasheqf1oi  14313  ccatcl  14536  cshwidxmodr  14766  wwlktovf1  14919  o1of2  15575  rlimsqzlem  15611  lcmgcdlem  16575  isprm5  16677  ramval  16979  mreexexlem4d  17613  acsfn  17625  chnso  18590  gsumpropd2lem  18647  issubmgm2  18671  gasubg  19277  omndmul2  20108  psgndiflemB  21580  psgndiflemA  21581  psrass1  21942  mhpmulcl  22115  mdetf  22560  cpmatacl  22681  cpmatinvcl  22682  mat2pmatf1  22694  mp2pm2mplem4  22774  chfacffsupp  22821  restcld  23137  cnpnei  23229  iscncl  23234  cncls  23239  cnntr  23240  1stcfb  23410  2ndcdisj  23421  txlly  23601  fbflim  23941  fclsbas  23986  nmoi  24693  mpomulcn  24834  fgcfil  25238  equivcau  25267  cmetcusp  25321  itg2cnlem1  25728  iblss  25772  lgsqr  27314  lgsqrmodndvds  27316  noetainflem4  27704  lesrec  27791  remulscllem2  28493  axcontlem2  29034  nbuhgr  29412  nbusgrvtxm1  29448  2pthon3v  30011  clwwisshclwwslem  30084  wwlksext2clwwlk  30127  2pthfrgr  30354  vdgn1frgrv2  30366  frgrwopreg  30393  numclwlk2lem2f1o  30449  blocnilem  30875  mdslmd3i  32403  foresf1o  32574  2ndresdju  32722  fgreu  32744  fdifsuppconst  32762  resf1o  32803  sgnmul  32908  psgnfzto1st  33166  elrgspnsubrunlem1  33308  isdrng4  33356  nsgqusf1olem3  33475  elrspunidl  33488  elrspunsn  33489  qsidomlem1  33512  1arithidom  33597  dfufd2lem  33609  mplvrpmga  33689  lbsdiflsp0  33770  evls1fldgencl  33814  cos9thpiminplylem2  33927  ist0cld  33977  locfinreflem  33984  cmpcref  33994  zarclsun  34014  pstmxmet  34041  lmdvg  34097  carsgclctunlem3  34464  oddpwdc  34498  signstres  34719  tgoldbachgtd  34806  cvmlift2lem12  35496  satfdmlem  35550  satffunlem2lem1  35586  mrsubff  35694  elicc3  36499  nn0prpwlem  36504  neibastop2  36543  neibastop3  36544  bj-prmoore  37427  ltflcei  37929  matunitlindflem2  37938  poimirlem4  37945  poimirlem13  37954  poimirlem14  37955  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  poimirlem29  37970  poimirlem31  37972  heicant  37976  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  itg2addnclem  37992  itg2addnclem2  37993  itg2addnclem3  37994  itg2addnc  37995  itg2gt0cn  37996  ftc1cnnc  38013  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  nnubfi  38071  nninfnub  38072  linepsubN  40198  lhpmatb  40477  cdlemf2  41008  diaglbN  41501  diaintclN  41504  dibglbN  41612  dibintclN  41613  dihlsscpre  41680  dihglblem5aN  41738  dihglblem2aN  41739  dih1dimatlem  41775  sticksstones12a  42596  fsuppind  43023  diophren  43241  irrapxlem2  43251  irrapxlem4  43253  wepwsolem  43470  omlimcl2  43670  tfsconcatfv  43769  ofoafg  43782  prmunb2  44738  cvgdvgrat  44740  fiiuncl  45496  infleinflem2  45800  supxrunb3  45828  supminfxr  45892  limsuppnflem  46138  limsupmnflem  46148  limsupre3lem  46160  dfxlim2v  46275  icccncfext  46315  ioodvbdlimc1lem1  46359  iblcncfioo  46406  wallispilem3  46495  fourierdlem12  46547  fourierdlem34  46569  fourierdlem50  46584  fourierdlem51  46585  fourierdlem65  46599  fourierdlem77  46611  meaiuninc3v  46912  hspdifhsp  47044  smflimlem4  47202  iccpartigtl  47877  iccpartgt  47881  fargshiftfva  47897  sfprmdvdsmersenne  48060  opoeALTV  48153  opeoALTV  48154  nnsum4primeseven  48270  nnsum4primesevenALTV  48271  uhgrimedgi  48360  isuspgrimlem  48365  gricushgr  48387  isubgr3stgrlem7  48442  uspgrlimlem4  48461  gpgedgvtx1  48532  pgn4cyclex  48596  uzlidlring  48705  2zrngmmgm  48722  cznrng  48731  ply1mulgsumlem2  48857  snlindsntor  48941  elbigo2  49022  nn0sumshdiglemA  49089  precofvalALT  49837