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  5086  fimaproj  8060  tfrlem1  8290  oaass  8471  acndom2  9937  infxp  10097  isf32lem2  10237  ttukeylem3  10394  gchina  10582  r1limwun  10619  difreicc  13376  ssfzo12bi  13653  flflp1  13703  hasheqf1oi  14250  ccatcl  14473  cshwidxmodr  14703  wwlktovf1  14856  o1of2  15512  rlimsqzlem  15548  lcmgcdlem  16509  isprm5  16610  ramval  16912  mreexexlem4d  17545  acsfn  17557  chnso  18522  gsumpropd2lem  18579  issubmgm2  18603  gasubg  19207  omndmul2  20038  psgndiflemB  21530  psgndiflemA  21531  psrass1  21894  mhpmulcl  22057  mdetf  22503  cpmatacl  22624  cpmatinvcl  22625  mat2pmatf1  22637  mp2pm2mplem4  22717  chfacffsupp  22764  restcld  23080  cnpnei  23172  iscncl  23177  cncls  23182  cnntr  23183  1stcfb  23353  2ndcdisj  23364  txlly  23544  fbflim  23884  fclsbas  23929  nmoi  24636  mpomulcn  24778  fgcfil  25191  equivcau  25220  cmetcusp  25274  itg2cnlem1  25682  iblss  25726  lgsqr  27282  lgsqrmodndvds  27284  noetainflem4  27672  slerec  27753  remulscllem2  28396  axcontlem2  28936  nbuhgr  29314  nbusgrvtxm1  29350  2pthon3v  29914  clwwisshclwwslem  29984  wwlksext2clwwlk  30027  2pthfrgr  30254  vdgn1frgrv2  30266  frgrwopreg  30293  numclwlk2lem2f1o  30349  blocnilem  30774  mdslmd3i  32302  foresf1o  32474  2ndresdju  32621  fgreu  32644  fdifsuppconst  32660  resf1o  32703  sgnmul  32808  psgnfzto1st  33064  elrgspnsubrunlem1  33204  isdrng4  33251  nsgqusf1olem3  33370  elrspunidl  33383  elrspunsn  33384  qsidomlem1  33407  1arithidom  33492  dfufd2lem  33504  mplvrpmga  33565  lbsdiflsp0  33629  evls1fldgencl  33673  cos9thpiminplylem2  33786  ist0cld  33836  locfinreflem  33843  cmpcref  33853  zarclsun  33873  pstmxmet  33900  lmdvg  33956  carsgclctunlem3  34323  oddpwdc  34357  signstres  34578  tgoldbachgtd  34665  cvmlift2lem12  35326  satfdmlem  35380  satffunlem2lem1  35416  mrsubff  35524  elicc3  36330  nn0prpwlem  36335  neibastop2  36374  neibastop3  36375  bj-prmoore  37128  ltflcei  37627  matunitlindflem2  37636  poimirlem4  37643  poimirlem13  37652  poimirlem14  37653  poimirlem26  37665  poimirlem27  37666  poimirlem28  37667  poimirlem29  37668  poimirlem31  37670  heicant  37674  mblfinlem2  37677  mblfinlem3  37678  mblfinlem4  37679  ismblfin  37680  itg2addnclem  37690  itg2addnclem2  37691  itg2addnclem3  37692  itg2addnc  37693  itg2gt0cn  37694  ftc1cnnc  37711  ftc1anclem5  37716  ftc1anclem6  37717  ftc1anclem7  37718  ftc1anclem8  37719  ftc1anc  37720  nnubfi  37769  nninfnub  37770  linepsubN  39770  lhpmatb  40049  cdlemf2  40580  diaglbN  41073  diaintclN  41076  dibglbN  41184  dibintclN  41185  dihlsscpre  41252  dihglblem5aN  41310  dihglblem2aN  41311  dih1dimatlem  41347  sticksstones12a  42169  fsuppind  42602  diophren  42825  irrapxlem2  42835  irrapxlem4  42837  wepwsolem  43054  omlimcl2  43254  tfsconcatfv  43353  ofoafg  43366  prmunb2  44323  cvgdvgrat  44325  fiiuncl  45081  infleinflem2  45388  supxrunb3  45416  supminfxr  45481  limsuppnflem  45727  limsupmnflem  45737  limsupre3lem  45749  dfxlim2v  45864  icccncfext  45904  ioodvbdlimc1lem1  45948  iblcncfioo  45995  wallispilem3  46084  fourierdlem12  46136  fourierdlem34  46158  fourierdlem50  46173  fourierdlem51  46174  fourierdlem65  46188  fourierdlem77  46200  meaiuninc3v  46501  hoicvr  46565  hspdifhsp  46633  smflimlem4  46791  iccpartigtl  47433  iccpartgt  47437  fargshiftfva  47453  sfprmdvdsmersenne  47613  opoeALTV  47693  opeoALTV  47694  nnsum4primeseven  47810  nnsum4primesevenALTV  47811  uhgrimedgi  47900  isuspgrimlem  47905  gricushgr  47927  isubgr3stgrlem7  47982  uspgrlimlem4  48001  gpgedgvtx1  48072  pgn4cyclex  48136  uzlidlring  48245  2zrngmmgm  48262  cznrng  48271  ply1mulgsumlem2  48398  snlindsntor  48482  elbigo2  48563  nn0sumshdiglemA  48630  precofvalALT  49379