Theorem ad3antlr 743

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  simpllr  787  disjxiun  5105  fimaproj  8130  tfrlem1  8361  oaass  8545  acndom2  10037  infxp  10196  isf32lem2  10337  ttukeylem3  10494  gchina  10683  r1limwun  10720  difreicc  13510  ssfzo12bi  13790  flflp1  13840  hasheqf1oi  14387  ccatcl  14611  cshwidxmodr  14841  wwlktovf1  14994  sgnmul  15144  o1of2  15664  rlimsqzlem  15700  lcmgcdlem  16663  isprm5  16765  ramval  17067  mreexexlem4d  17702  acsfn  17714  chnso  18679  gsumpropd2lem  18736  issubmgm2  18760  gasubg  19371  omndmul2  20202  isdrng4  20824  unichnlidl  21341  qsidomlem1  21459  psgndiflemB  21729  psgndiflemA  21730  psrass1  22092  mhpmulcl  22291  mdetf  22731  cpmatacl  22852  cpmatinvcl  22853  mat2pmatf1  22865  mp2pm2mplem4  22945  chfacffsupp  22992  restcld  23308  cnpnei  23400  iscncl  23405  cncls  23410  cnntr  23411  1stcfb  23581  2ndcdisj  23592  txlly  23772  fbflim  24112  fclsbas  24157  nmoi  24864  mpomulcn  25005  fgcfil  25409  equivcau  25438  cmetcusp  25492  itg2cnlem1  25899  iblss  25943  lgsqr  27491  lgsqrmodndvds  27493  noetainflem4  27880  lesrec  27968  remulscllem2  28670  axcontlem2  29281  nbuhgr  29659  nbusgrvtxm1  29695  2pthon3v  30258  clwwisshclwwslem  30331  wwlksext2clwwlk  30374  2pthfrgr  30601  vdgn1frgrv2  30613  frgrwopreg  30640  numclwlk2lem2f1o  30696  blocnilem  31122  mdslmd3i  32650  foresf1o  32816  2ndresdju  32960  fgreu  32982  fdifsuppconst  33000  resf1o  33041  psgnfzto1st  33391  elrgspnsubrunlem1  33533  nsgqusf1olem3  33690  elrspunidl  33702  elrspunsn  33703  dflringlem3  33752  dflring4  33754  1arithidom  33793  dfufd2lem  33805  mplvrpmga  33901  lbsdiflsp0  33982  evls1fldgencl  34026  cos9thpiminplylem2  34139  ist0cld  34189  locfinreflem  34196  cmpcref  34206  zarclsun  34226  pstmxmet  34253  lmdvg  34309  carsgclctunlem3  34676  oddpwdc  34710  signstres  34928  tgoldbachgtd  35015  cvmlift2lem12  35772  satfdmlem  35826  satffunlem2lem1  35862  mrsubff  35970  elicc3  36794  nn0prpwlem  36799  neibastop2  36838  neibastop3  36839  bj-prmoore  37723  ltflcei  38225  matunitlindflem2  38234  poimirlem4  38241  poimirlem13  38250  poimirlem14  38251  poimirlem26  38263  poimirlem27  38264  poimirlem28  38265  poimirlem29  38266  poimirlem31  38268  heicant  38272  mblfinlem2  38275  mblfinlem3  38276  mblfinlem4  38277  ismblfin  38278  itg2addnclem  38288  itg2addnclem2  38289  itg2addnclem3  38290  itg2addnc  38291  itg2gt0cn  38292  ftc1cnnc  38309  ftc1anclem5  38314  ftc1anclem6  38315  ftc1anclem7  38316  ftc1anclem8  38317  ftc1anc  38318  nnubfi  38367  nninfnub  38368  linepsubN  40494  lhpmatb  40773  cdlemf2  41304  diaglbN  41797  diaintclN  41800  dibglbN  41908  dibintclN  41909  dihlsscpre  41976  dihglblem5aN  42034  dihglblem2aN  42035  dih1dimatlem  42071  sticksstones12a  42892  fsuppind  43292  diophren  43510  irrapxlem2  43520  irrapxlem4  43522  wepwsolem  43739  omlimcl2  43939  tfsconcatfv  44038  ofoafg  44051  prmunb2  44991  cvgdvgrat  44993  fiiuncl  45755  infleinflem2  46056  supxrunb3  46084  supminfxr  46148  limsuppnflem  46394  limsupmnflem  46404  limsupre3lem  46416  dfxlim2v  46531  icccncfext  46571  ioodvbdlimc1lem1  46615  iblcncfioo  46662  wallispilem3  46751  fourierdlem12  46803  fourierdlem34  46825  fourierdlem50  46840  fourierdlem51  46841  fourierdlem65  46855  fourierdlem77  46867  meaiuninc3v  47168  hspdifhsp  47300  smflimlem4  47458  iccpartigtl  48139  iccpartgt  48143  fargshiftfva  48159  sfprmdvdsmersenne  48322  opoeALTV  48415  opeoALTV  48416  nnsum4primeseven  48532  nnsum4primesevenALTV  48533  uhgrimedgi  48622  isuspgrimlem  48627  gricushgr  48649  isubgr3stgrlem7  48704  uspgrlimlem4  48723  gpgedgvtx1  48794  pgn4cyclex  48858  uzlidlring  48967  2zrngmmgm  48984  cznrng  48993  ply1mulgsumlem2  49134  snlindsntor  49218  elbigo2  49299  nn0sumshdiglemA  49366  precofvalALT  50113