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  775  disjxiun  5092  fimaproj  8074  tfrlem1  8304  oaass  8485  acndom2  9955  infxp  10115  isf32lem2  10255  ttukeylem3  10412  gchina  10600  r1limwun  10637  difreicc  13394  ssfzo12bi  13671  flflp1  13721  hasheqf1oi  14268  ccatcl  14491  cshwidxmodr  14721  wwlktovf1  14874  o1of2  15530  rlimsqzlem  15566  lcmgcdlem  16527  isprm5  16628  ramval  16930  mreexexlem4d  17563  acsfn  17575  chnso  18540  gsumpropd2lem  18597  issubmgm2  18621  gasubg  19224  omndmul2  20055  psgndiflemB  21547  psgndiflemA  21548  psrass1  21911  mhpmulcl  22074  mdetf  22520  cpmatacl  22641  cpmatinvcl  22642  mat2pmatf1  22654  mp2pm2mplem4  22734  chfacffsupp  22781  restcld  23097  cnpnei  23189  iscncl  23194  cncls  23199  cnntr  23200  1stcfb  23370  2ndcdisj  23381  txlly  23561  fbflim  23901  fclsbas  23946  nmoi  24653  mpomulcn  24795  fgcfil  25208  equivcau  25237  cmetcusp  25291  itg2cnlem1  25699  iblss  25743  lgsqr  27299  lgsqrmodndvds  27301  noetainflem4  27689  slerec  27770  remulscllem2  28413  axcontlem2  28954  nbuhgr  29332  nbusgrvtxm1  29368  2pthon3v  29932  clwwisshclwwslem  30005  wwlksext2clwwlk  30048  2pthfrgr  30275  vdgn1frgrv2  30287  frgrwopreg  30314  numclwlk2lem2f1o  30370  blocnilem  30795  mdslmd3i  32323  foresf1o  32495  2ndresdju  32642  fgreu  32665  fdifsuppconst  32681  resf1o  32724  sgnmul  32829  psgnfzto1st  33085  elrgspnsubrunlem1  33225  isdrng4  33272  nsgqusf1olem3  33391  elrspunidl  33404  elrspunsn  33405  qsidomlem1  33428  1arithidom  33513  dfufd2lem  33525  mplvrpmga  33586  lbsdiflsp0  33650  evls1fldgencl  33694  cos9thpiminplylem2  33807  ist0cld  33857  locfinreflem  33864  cmpcref  33874  zarclsun  33894  pstmxmet  33921  lmdvg  33977  carsgclctunlem3  34344  oddpwdc  34378  signstres  34599  tgoldbachgtd  34686  cvmlift2lem12  35369  satfdmlem  35423  satffunlem2lem1  35459  mrsubff  35567  elicc3  36372  nn0prpwlem  36377  neibastop2  36416  neibastop3  36417  bj-prmoore  37170  ltflcei  37658  matunitlindflem2  37667  poimirlem4  37674  poimirlem13  37683  poimirlem14  37684  poimirlem26  37696  poimirlem27  37697  poimirlem28  37698  poimirlem29  37699  poimirlem31  37701  heicant  37705  mblfinlem2  37708  mblfinlem3  37709  mblfinlem4  37710  ismblfin  37711  itg2addnclem  37721  itg2addnclem2  37722  itg2addnclem3  37723  itg2addnc  37724  itg2gt0cn  37725  ftc1cnnc  37742  ftc1anclem5  37747  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751  nnubfi  37800  nninfnub  37801  linepsubN  39861  lhpmatb  40140  cdlemf2  40671  diaglbN  41164  diaintclN  41167  dibglbN  41275  dibintclN  41276  dihlsscpre  41343  dihglblem5aN  41401  dihglblem2aN  41402  dih1dimatlem  41438  sticksstones12a  42260  fsuppind  42698  diophren  42920  irrapxlem2  42930  irrapxlem4  42932  wepwsolem  43149  omlimcl2  43349  tfsconcatfv  43448  ofoafg  43461  prmunb2  44418  cvgdvgrat  44420  fiiuncl  45176  infleinflem2  45483  supxrunb3  45511  supminfxr  45576  limsuppnflem  45822  limsupmnflem  45832  limsupre3lem  45844  dfxlim2v  45959  icccncfext  45999  ioodvbdlimc1lem1  46043  iblcncfioo  46090  wallispilem3  46179  fourierdlem12  46231  fourierdlem34  46253  fourierdlem50  46268  fourierdlem51  46269  fourierdlem65  46283  fourierdlem77  46295  meaiuninc3v  46596  hoicvr  46660  hspdifhsp  46728  smflimlem4  46886  iccpartigtl  47537  iccpartgt  47541  fargshiftfva  47557  sfprmdvdsmersenne  47717  opoeALTV  47797  opeoALTV  47798  nnsum4primeseven  47914  nnsum4primesevenALTV  47915  uhgrimedgi  48004  isuspgrimlem  48009  gricushgr  48031  isubgr3stgrlem7  48086  uspgrlimlem4  48105  gpgedgvtx1  48176  pgn4cyclex  48240  uzlidlring  48349  2zrngmmgm  48366  cznrng  48375  ply1mulgsumlem2  48502  snlindsntor  48586  elbigo2  48667  nn0sumshdiglemA  48734  precofvalALT  49483