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 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

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

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 401

This theorem is used by:  simpllr  787  disjxiun  5105  fimaproj  8129  tfrlem1  8360  oaass  8544  acndom2  10045  infxp  10204  isf32lem2  10344  ttukeylem3  10501  gchina  10690  r1limwun  10727  difreicc  13517  ssfzo12bi  13797  flflp1  13847  hasheqf1oi  14394  ccatcl  14618  cshwidxmodr  14848  wwlktovf1  15001  sgnmul  15151  o1of2  15671  rlimsqzlem  15707  lcmgcdlem  16670  isprm5  16772  ramval  17074  mreexexlem4d  17709  acsfn  17721  chnso  18686  gsumpropd2lem  18743  issubmgm2  18767  gasubg  19378  omndmul2  20209  isdrng4  20850  unichnlidl  21373  qsidomlem1  21491  psgndiflemB  21761  psgndiflemA  21762  psrass1  22124  mhpmulcl  22323  mdetf  22763  cpmatacl  22884  cpmatinvcl  22885  mat2pmatf1  22897  mp2pm2mplem4  22977  chfacffsupp  23024  restcld  23340  cnpnei  23432  iscncl  23437  cncls  23442  cnntr  23443  1stcfb  23613  2ndcdisj  23624  txlly  23804  fbflim  24144  fclsbas  24189  nmoi  24896  mpomulcn  25037  fgcfil  25441  equivcau  25470  cmetcusp  25524  itg2cnlem1  25931  iblss  25975  lgsqr  27526  lgsqrmodndvds  27528  noetainflem4  27915  lesrec  28003  remulscllem2  28705  axcontlem2  29326  nbuhgr  29704  nbusgrvtxm1  29740  2pthon3v  30303  clwwisshclwwslem  30376  wwlksext2clwwlk  30419  2pthfrgr  30646  vdgn1frgrv2  30658  frgrwopreg  30685  numclwlk2lem2f1o  30741  blocnilem  31167  mdslmd3i  32695  foresf1o  32861  2ndresdju  33005  fgreu  33027  fdifsuppconst  33045  resf1o  33086  psgnfzto1st  33434  elrgspnsubrunlem1  33576  nsgqusf1olem3  33733  elrspunidl  33745  elrspunsn  33746  dflringlem3  33795  dflring4  33797  1arithidom  33836  dfufd2lem  33848  mplvrpmga  33944  lbsdiflsp0  34025  evls1fldgencl  34069  cos9thpiminplylem2  34182  ist0cld  34232  locfinreflem  34239  cmpcref  34249  zarclsun  34269  pstmxmet  34296  lmdvg  34352  carsgclctunlem3  34719  oddpwdc  34753  signstres  34971  tgoldbachgtd  35058  cvmlift2lem12  35814  satfdmlem  35868  satffunlem2lem1  35904  mrsubff  36012  elicc3  36856  nn0prpwlem  36861  neibastop2  36900  neibastop3  36901  bj-prmoore  37785  ltflcei  38287  matunitlindflem2  38296  poimirlem4  38303  poimirlem13  38312  poimirlem14  38313  poimirlem26  38325  poimirlem27  38326  poimirlem28  38327  poimirlem29  38328  poimirlem31  38330  heicant  38334  mblfinlem2  38337  mblfinlem3  38338  mblfinlem4  38339  ismblfin  38340  itg2addnclem  38350  itg2addnclem2  38351  itg2addnclem3  38352  itg2addnc  38353  itg2gt0cn  38354  ftc1cnnc  38371  ftc1anclem5  38376  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  nnubfi  38429  nninfnub  38430  linepsubN  40554  lhpmatb  40833  cdlemf2  41364  diaglbN  41857  diaintclN  41860  dibglbN  41968  dibintclN  41969  dihlsscpre  42036  dihglblem5aN  42094  dihglblem2aN  42095  dih1dimatlem  42131  sticksstones12a  42952  fsuppind  43350  diophren  43568  irrapxlem2  43578  irrapxlem4  43580  wepwsolem  43797  omlimcl2  43997  tfsconcatfv  44096  ofoafg  44109  prmunb2  45049  cvgdvgrat  45051  fiiuncl  45813  infleinflem2  46114  supxrunb3  46142  supminfxr  46206  limsuppnflem  46452  limsupmnflem  46462  limsupre3lem  46474  dfxlim2v  46589  icccncfext  46629  ioodvbdlimc1lem1  46673  iblcncfioo  46720  wallispilem3  46809  fourierdlem12  46861  fourierdlem34  46883  fourierdlem50  46898  fourierdlem51  46899  fourierdlem65  46913  fourierdlem77  46925  meaiuninc3v  47226  hspdifhsp  47358  smflimlem4  47516  iccpartigtl  48200  iccpartgt  48204  fargshiftfva  48220  sfprmdvdsmersenne  48383  opoeALTV  48476  opeoALTV  48477  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  uhgrimedgi  48683  isuspgrimlem  48688  gricushgr  48710  isubgr3stgrlem7  48765  uspgrlimlem4  48784  gpgedgvtx1  48855  pgn4cyclex  48919  uzlidlring  49028  2zrngmmgm  49045  cznrng  49054  ply1mulgsumlem2  49195  snlindsntor  49279  elbigo2  49360  nn0sumshdiglemA  49427  precofvalALT  50174