Theorem ad3antlr 744

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

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

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 402

This theorem is used by:  simpllr  788  disjxiun  5104  fimaproj  8137  tfrlem1  8368  oaass  8552  acndom2  10061  infxp  10220  isf32lem2  10360  ttukeylem3  10517  gchina  10712  r1limwun  10749  difreicc  13541  ssfzo12bi  13821  flflp1  13872  hasheqf1oi  14419  ccatcl  14643  cshwidxmodr  14879  wwlktovf1  15034  sgnmul  15184  o1of2  15704  rlimsqzlem  15740  lcmgcdlem  16702  isprm5  16804  ramval  17106  mreexexlem4d  17741  acsfn  17753  chnso  18718  gsumpropd2lem  18787  issubmgm2  18811  gasubg  19435  omndmul2  20266  isdrng4  20908  unichnlidl  21431  qsidomlem1  21549  psgndiflemB  21819  psgndiflemA  21820  psrass1  22184  mhpmulcl  22383  mdetf  22823  matunitlindflem2  22908  cpmatacl  22947  cpmatinvcl  22948  mat2pmatf1  22960  mp2pm2mplem4  23040  chfacffsupp  23087  restcld  23403  cnpnei  23495  iscncl  23500  cncls  23505  cnntr  23506  1stcfb  23676  2ndcdisj  23688  txlly  23868  fbflim  24208  fclsbas  24253  nmoi  24960  mpomulcn  25101  fgcfil  25505  equivcau  25534  cmetcusp  25588  itg2cnlem1  25995  iblss  26039  lgsqr  27595  lgsqrmodndvds  27597  noetainflem4  27984  lesrec  28072  remulscllem2  28774  axcontlem2  29430  nbuhgr  29811  nbusgrvtxm1  29847  2pthon3v  30419  clwwisshclwwslem  30492  wwlksext2clwwlk  30535  2pthfrgr  30772  vdgn1frgrv2  30784  frgrwopreg  30811  numclwlk2lem2f1o  30867  blocnilem  31293  mdslmd3i  32821  foresf1o  32987  2ndresdju  33130  fgreu  33152  fdifsuppconst  33169  resf1o  33209  psgnfzto1st  33553  elrgspnsubrunlem1  33695  nsgqusf1olem3  33852  elrspunidl  33864  elrspunsn  33865  dflringlem3  33914  dflring4  33916  1arithidom  33955  dfufd2lem  33967  mplvrpmga  34063  lbsdiflsp0  34144  evls1fldgencl  34188  cos9thpiminplylem2  34301  ist0cld  34351  locfinreflem  34358  cmpcref  34368  zarclsun  34388  pstmxmet  34415  lmdvg  34471  carsgclctunlem3  34839  oddpwdc  34873  signstres  35091  tgoldbachgtd  35178  cvmlift2lem12  35901  satfdmlem  35955  satffunlem2lem1  35991  mrsubff  36099  elicc3  36944  nn0prpwlem  36949  neibastop2  36988  neibastop3  36989  bj-prmoore  37873  ltflcei  38370  poimirlem4  38381  poimirlem13  38390  poimirlem14  38391  poimirlem26  38403  poimirlem27  38404  poimirlem28  38405  poimirlem29  38406  poimirlem31  38408  heicant  38412  mblfinlem2  38415  mblfinlem3  38416  mblfinlem4  38417  ismblfin  38418  itg2addnclem  38428  itg2addnclem2  38429  itg2addnclem3  38430  itg2addnc  38431  itg2gt0cn  38432  ftc1cnnc  38449  ftc1anclem5  38454  ftc1anclem6  38455  ftc1anclem7  38456  ftc1anclem8  38457  ftc1anc  38458  nnubfi  38508  nninfnub  38509  linepsubN  40633  lhpmatb  40912  cdlemf2  41443  diaglbN  41936  diaintclN  41939  dibglbN  42047  dibintclN  42048  dihlsscpre  42115  dihglblem5aN  42173  dihglblem2aN  42174  dih1dimatlem  42210  sticksstones12a  43031  fsuppind  43444  diophren  43662  irrapxlem2  43672  irrapxlem4  43674  wepwsolem  43891  omlimcl2  44091  tfsconcatfv  44190  ofoafg  44203  prmunb2  45143  cvgdvgrat  45145  fiiuncl  45907  infleinflem2  46208  supxrunb3  46236  supminfxr  46300  limsuppnflem  46546  limsupmnflem  46556  limsupre3lem  46568  dfxlim2v  46683  icccncfext  46723  ioodvbdlimc1lem1  46767  iblcncfioo  46814  wallispilem3  46903  fourierdlem12  46955  fourierdlem34  46977  fourierdlem50  46992  fourierdlem51  46993  fourierdlem65  47007  fourierdlem77  47019  meaiuninc3v  47320  hspdifhsp  47452  smflimlem4  47610  iccpartigtl  48331  iccpartgt  48335  fargshiftfva  48351  sfprmdvdsmersenne  48514  opoeALTV  48607  opeoALTV  48608  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  uhgrimedgi  48814  isuspgrimlem  48819  gricushgr  48841  isubgr3stgrlem7  48896  uspgrlimlem4  48915  gpgedgvtx1  48986  pgn4cyclex  49050  uzlidlring  49158  2zrngmmgm  49175  cznrng  49184  ply1mulgsumlem2  49325  snlindsntor  49409  elbigo2  49490  nn0sumshdiglemA  49557  precofvalALT  50302