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  5097  fimaproj  8087  tfrlem1  8317  oaass  8498  acndom2  9976  infxp  10136  isf32lem2  10276  ttukeylem3  10433  gchina  10622  r1limwun  10659  difreicc  13412  ssfzo12bi  13689  flflp1  13739  hasheqf1oi  14286  ccatcl  14509  cshwidxmodr  14739  wwlktovf1  14892  o1of2  15548  rlimsqzlem  15584  lcmgcdlem  16545  isprm5  16646  ramval  16948  mreexexlem4d  17582  acsfn  17594  chnso  18559  gsumpropd2lem  18616  issubmgm2  18640  gasubg  19243  omndmul2  20074  psgndiflemB  21567  psgndiflemA  21568  psrass1  21931  mhpmulcl  22104  mdetf  22551  cpmatacl  22672  cpmatinvcl  22673  mat2pmatf1  22685  mp2pm2mplem4  22765  chfacffsupp  22812  restcld  23128  cnpnei  23220  iscncl  23225  cncls  23230  cnntr  23231  1stcfb  23401  2ndcdisj  23412  txlly  23592  fbflim  23932  fclsbas  23977  nmoi  24684  mpomulcn  24826  fgcfil  25239  equivcau  25268  cmetcusp  25322  itg2cnlem1  25730  iblss  25774  lgsqr  27330  lgsqrmodndvds  27332  noetainflem4  27720  lesrec  27807  remulscllem2  28509  axcontlem2  29050  nbuhgr  29428  nbusgrvtxm1  29464  2pthon3v  30028  clwwisshclwwslem  30101  wwlksext2clwwlk  30144  2pthfrgr  30371  vdgn1frgrv2  30383  frgrwopreg  30410  numclwlk2lem2f1o  30466  blocnilem  30891  mdslmd3i  32419  foresf1o  32590  2ndresdju  32738  fgreu  32760  fdifsuppconst  32778  resf1o  32819  sgnmul  32926  psgnfzto1st  33198  elrgspnsubrunlem1  33340  isdrng4  33388  nsgqusf1olem3  33507  elrspunidl  33520  elrspunsn  33521  qsidomlem1  33544  1arithidom  33629  dfufd2lem  33641  mplvrpmga  33721  lbsdiflsp0  33803  evls1fldgencl  33847  cos9thpiminplylem2  33960  ist0cld  34010  locfinreflem  34017  cmpcref  34027  zarclsun  34047  pstmxmet  34074  lmdvg  34130  carsgclctunlem3  34497  oddpwdc  34531  signstres  34752  tgoldbachgtd  34839  cvmlift2lem12  35527  satfdmlem  35581  satffunlem2lem1  35617  mrsubff  35725  elicc3  36530  nn0prpwlem  36535  neibastop2  36574  neibastop3  36575  bj-prmoore  37359  ltflcei  37848  matunitlindflem2  37857  poimirlem4  37864  poimirlem13  37873  poimirlem14  37874  poimirlem26  37886  poimirlem27  37887  poimirlem28  37888  poimirlem29  37889  poimirlem31  37891  heicant  37895  mblfinlem2  37898  mblfinlem3  37899  mblfinlem4  37900  ismblfin  37901  itg2addnclem  37911  itg2addnclem2  37912  itg2addnclem3  37913  itg2addnc  37914  itg2gt0cn  37915  ftc1cnnc  37932  ftc1anclem5  37937  ftc1anclem6  37938  ftc1anclem7  37939  ftc1anclem8  37940  ftc1anc  37941  nnubfi  37990  nninfnub  37991  linepsubN  40117  lhpmatb  40396  cdlemf2  40927  diaglbN  41420  diaintclN  41423  dibglbN  41531  dibintclN  41532  dihlsscpre  41599  dihglblem5aN  41657  dihglblem2aN  41658  dih1dimatlem  41694  sticksstones12a  42516  fsuppind  42937  diophren  43159  irrapxlem2  43169  irrapxlem4  43171  wepwsolem  43388  omlimcl2  43588  tfsconcatfv  43687  ofoafg  43700  prmunb2  44656  cvgdvgrat  44658  fiiuncl  45414  infleinflem2  45718  supxrunb3  45746  supminfxr  45811  limsuppnflem  46057  limsupmnflem  46067  limsupre3lem  46079  dfxlim2v  46194  icccncfext  46234  ioodvbdlimc1lem1  46278  iblcncfioo  46325  wallispilem3  46414  fourierdlem12  46466  fourierdlem34  46488  fourierdlem50  46503  fourierdlem51  46504  fourierdlem65  46518  fourierdlem77  46530  meaiuninc3v  46831  hoicvr  46895  hspdifhsp  46963  smflimlem4  47121  iccpartigtl  47772  iccpartgt  47776  fargshiftfva  47792  sfprmdvdsmersenne  47952  opoeALTV  48032  opeoALTV  48033  nnsum4primeseven  48149  nnsum4primesevenALTV  48150  uhgrimedgi  48239  isuspgrimlem  48244  gricushgr  48266  isubgr3stgrlem7  48321  uspgrlimlem4  48340  gpgedgvtx1  48411  pgn4cyclex  48475  uzlidlring  48584  2zrngmmgm  48601  cznrng  48610  ply1mulgsumlem2  48736  snlindsntor  48820  elbigo2  48901  nn0sumshdiglemA  48968  precofvalALT  49716