Theorem ad3antlr 731

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 726	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  5140  fimaproj  8160  tfrlem1  8416  oaass  8599  undomOLD  9100  acndom2  10094  infxp  10254  isf32lem2  10394  ttukeylem3  10551  gchina  10739  r1limwun  10776  difreicc  13524  ssfzo12bi  13800  flflp1  13847  hasheqf1oi  14390  ccatcl  14612  cshwidxmodr  14842  wwlktovf1  14996  o1of2  15649  rlimsqzlem  15685  lcmgcdlem  16643  isprm5  16744  ramval  17046  mreexexlem4d  17690  acsfn  17702  gsumpropd2lem  18692  issubmgm2  18716  gasubg  19320  psgndiflemB  21618  psgndiflemA  21619  psrass1  21984  mhpmulcl  22153  mdetf  22601  cpmatacl  22722  cpmatinvcl  22723  mat2pmatf1  22735  mp2pm2mplem4  22815  chfacffsupp  22862  restcld  23180  cnpnei  23272  iscncl  23277  cncls  23282  cnntr  23283  1stcfb  23453  2ndcdisj  23464  txlly  23644  fbflim  23984  fclsbas  24029  nmoi  24749  mpomulcn  24891  fgcfil  25305  equivcau  25334  cmetcusp  25388  itg2cnlem1  25796  iblss  25840  lgsqr  27395  lgsqrmodndvds  27397  noetainflem4  27785  slerec  27864  remulscllem2  28433  axcontlem2  28980  nbuhgr  29360  nbusgrvtxm1  29396  2pthon3v  29963  clwwisshclwwslem  30033  wwlksext2clwwlk  30076  2pthfrgr  30303  vdgn1frgrv2  30315  frgrwopreg  30342  numclwlk2lem2f1o  30398  blocnilem  30823  mdslmd3i  32351  foresf1o  32523  2ndresdju  32659  fgreu  32682  fdifsuppconst  32698  resf1o  32741  chnso  33004  omndmul2  33089  psgnfzto1st  33125  elrgspnsubrunlem1  33251  isdrng4  33298  nsgqusf1olem3  33443  elrspunidl  33456  elrspunsn  33457  qsidomlem1  33480  1arithidom  33565  dfufd2lem  33577  lbsdiflsp0  33677  evls1fldgencl  33720  ist0cld  33832  locfinreflem  33839  cmpcref  33849  zarclsun  33869  pstmxmet  33896  lmdvg  33952  carsgclctunlem3  34322  oddpwdc  34356  sgnmul  34545  signstres  34590  tgoldbachgtd  34677  cvmlift2lem12  35319  satfdmlem  35373  satffunlem2lem1  35409  mrsubff  35517  elicc3  36318  nn0prpwlem  36323  neibastop2  36362  neibastop3  36363  bj-prmoore  37116  ltflcei  37615  matunitlindflem2  37624  poimirlem4  37631  poimirlem13  37640  poimirlem14  37641  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  poimirlem29  37656  poimirlem31  37658  heicant  37662  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  itg2addnclem  37678  itg2addnclem2  37679  itg2addnclem3  37680  itg2addnc  37681  itg2gt0cn  37682  ftc1cnnc  37699  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  nnubfi  37757  nninfnub  37758  linepsubN  39754  lhpmatb  40033  cdlemf2  40564  diaglbN  41057  diaintclN  41060  dibglbN  41168  dibintclN  41169  dihlsscpre  41236  dihglblem5aN  41294  dihglblem2aN  41295  dih1dimatlem  41331  sticksstones12a  42158  fsuppind  42600  diophren  42824  irrapxlem2  42834  irrapxlem4  42836  wepwsolem  43054  omlimcl2  43254  tfsconcatfv  43354  ofoafg  43367  prmunb2  44330  cvgdvgrat  44332  fiiuncl  45070  infleinflem2  45382  supxrunb3  45410  supminfxr  45475  limsuppnflem  45725  limsupmnflem  45735  limsupre3lem  45747  dfxlim2v  45862  icccncfext  45902  ioodvbdlimc1lem1  45946  iblcncfioo  45993  wallispilem3  46082  fourierdlem12  46134  fourierdlem34  46156  fourierdlem50  46171  fourierdlem51  46172  fourierdlem65  46186  fourierdlem77  46198  meaiuninc3v  46499  hoicvr  46563  hspdifhsp  46631  smflimlem4  46789  iccpartigtl  47410  iccpartgt  47414  fargshiftfva  47430  sfprmdvdsmersenne  47590  opoeALTV  47670  opeoALTV  47671  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  isuspgrimlem  47874  gricushgr  47886  isubgr3stgrlem7  47939  uspgrlimlem4  47958  gpgedgvtx1  48020  uzlidlring  48151  2zrngmmgm  48168  cznrng  48177  ply1mulgsumlem2  48304  snlindsntor  48388  elbigo2  48473  nn0sumshdiglemA  48540  precofvalALT  49063