Theorem ad3antlr 744

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simpllr  788  disjxiun  5103  fimaproj  8179  tfrlem1  8411  oaass  8597  acndom2  10160  infxp  10319  isf32lem2  10459  ttukeylem3  10616  gchina  10811  r1limwun  10848  difreicc  13642  ssfzo12bi  13923  flflp1  13974  hasheqf1oi  14522  ccatcl  14746  cshwidxmodr  14983  wwlktovf1  15139  sgnmul  15289  o1of2  15809  rlimsqzlem  15845  lcmgcdlem  16810  isprm5  16912  ramval  17215  mreexexlem4d  17850  acsfn  17862  chnso  18827  gsumpropd2lem  18897  issubmgm2  18921  gasubg  19546  omndmul2  20377  isdrng4  21022  unichnlidl  21546  qsidomlem1  21666  psgndiflemB  21936  psgndiflemA  21937  psrass1  22301  mhpmulcl  22500  mdetf  22940  matunitlindflem2  23025  cpmatacl  23064  cpmatinvcl  23065  mat2pmatf1  23077  mp2pm2mplem4  23157  chfacffsupp  23204  restcld  23520  cnpnei  23612  iscncl  23617  cncls  23622  cnntr  23623  1stcfb  23793  2ndcdisj  23805  txlly  23985  fbflim  24325  fclsbas  24370  nmoi  25077  mpomulcn  25218  fgcfil  25622  equivcau  25651  cmetcusp  25705  itg2cnlem1  26112  iblss  26155  lgsqr  27708  lgsqrmodndvds  27710  noetainflem4  28127  lesrec  28215  remulscllem2  28917  axcontlem2  29573  nbuhgr  29954  nbusgrvtxm1  29990  2pthon3v  30562  clwwisshclwwslem  30635  wwlksext2clwwlk  30678  2pthfrgr  30915  vdgn1frgrv2  30927  frgrwopreg  30954  numclwlk2lem2f1o  31010  blocnilem  31436  mdslmd3i  32964  foresf1o  33172  2ndresdju  33315  fgreu  33337  fdifsuppconst  33353  resf1o  33392  psgnfzto1st  33736  elrgspnsubrunlem1  33878  nsgqusf1olem3  34036  elrspunidl  34048  elrspunsn  34049  dflringlem3  34098  dflring4  34100  1arithidom  34139  dfufd2lem  34151  mplvrpmga  34247  lbsdiflsp0  34328  evls1fldgencl  34372  cos9thpiminplylem2  34485  ist0cld  34535  locfinreflem  34542  cmpcref  34552  zarclsun  34572  pstmxmet  34599  lmdvg  34655  carsgclctunlem3  35022  oddpwdc  35056  signstres  35274  tgoldbachgtd  35361  cvmlift2lem12  36246  satfdmlem  36300  satffunlem2lem1  36336  mrsubff  36444  elicc3  37283  nn0prpwlem  37288  neibastop2  37327  neibastop3  37328  mh-inf3f1  37507  bj-prmoore  38227  ltflcei  38723  poimirlem4  38734  poimirlem13  38743  poimirlem14  38744  poimirlem26  38756  poimirlem27  38757  poimirlem28  38758  poimirlem29  38759  poimirlem31  38761  heicant  38765  mblfinlem2  38768  mblfinlem3  38769  mblfinlem4  38770  ismblfin  38771  itg2addnclem  38781  itg2addnclem2  38782  itg2addnclem3  38783  itg2addnc  38784  itg2gt0cn  38785  ftc1cnnc  38802  ftc1anclem5  38807  ftc1anclem6  38808  ftc1anclem7  38809  ftc1anclem8  38810  ftc1anc  38811  nnubfi  38876  nninfnub  38877  linepsubN  41001  lhpmatb  41280  cdlemf2  41811  diaglbN  42304  diaintclN  42307  dibglbN  42415  dibintclN  42416  dihlsscpre  42483  dihglblem5aN  42541  dihglblem2aN  42542  dih1dimatlem  42578  sticksstones12a  43399  fsuppind  43811  diophren  44013  irrapxlem2  44023  irrapxlem4  44025  wepwsolem  44242  omlimcl2  44436  tfsconcatfv  44535  ofoafg  44548  prmunb2  45487  cvgdvgrat  45489  fiiuncl  46287  infleinflem2  46587  supxrunb3  46615  supminfxr  46679  limsuppnflem  46925  limsupmnflem  46935  limsupre3lem  46947  dfxlim2v  47062  icccncfext  47102  ioodvbdlimc1lem1  47146  iblcncfioo  47193  wallispilem3  47282  fourierdlem12  47334  fourierdlem34  47356  fourierdlem50  47371  fourierdlem51  47372  fourierdlem65  47386  fourierdlem77  47398  meaiuninc3v  47699  hspdifhsp  47831  smflimlem4  47989  iccpartigtl  48710  iccpartgt  48714  fargshiftfva  48730  sfprmdvdsmersenne  48893  opoeALTV  48986  opeoALTV  48987  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  uhgrimedgi  49193  isuspgrimlem  49198  gricushgr  49220  isubgr3stgrlem7  49275  uspgrlimlem4  49294  gpgedgvtx1  49365  pgn4cyclex  49429  uzlidlring  49537  2zrngmmgm  49554  cznrng  49563  ply1mulgsumlem2  49704  snlindsntor  49788  elbigo2  49869  nn0sumshdiglemA  49936  precofvalALT  50708