Theorem ad4ant13 748

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)

Hypothesis

Ref	Expression
ad4ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad4ant13	⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Proof of Theorem ad4ant13

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantr 480	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 716	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 206  df-an 396

This theorem is referenced by:  ad5ant14  755  ad5ant24  758  fntpb  7202  peano5  7877  peano5OLD  7878  f1o2ndf1  8102  cantnfle  9662  cantnflem1c  9678  ttukeylem5  10504  rlimsqzlem  15592  dvdslcmf  16565  poslubmo  18366  posglbmo  18367  smndex1mgm  18822  isgrpinv  18913  ghmgrp  18984  dprdfcntz  19927  pzriprnglem4  21339  sraassab  21730  cply1coe0bi  22143  isnrm3  23185  cnextcn  23893  ustexsym  24042  ustex2sym  24043  ustex3sym  24044  trust  24056  fmucnd  24119  trcfilu  24121  metust  24389  cxpmul2z  26541  umgrres1lem  29036  upgrres1  29039  friendshipgt3  30120  ccatf1  32582  cyc3evpm  32777  znfermltl  32948  rhmimaidl  33019  evls1fpws  33113  txomap  33303  zart0  33348  repr0  34112  breprexplemc  34133  hgt750lemb  34157  satffunlem1lem2  34883  satffunlem2lem2  34886  lindsadd  36971  matunitlindflem1  36974  nadd1suc  42631  mapss2  44389  supxrge  44533  xrlexaddrp  44547  infxr  44562  infleinf  44567  unb2ltle  44610  supminfxr  44659  limsuppnfdlem  44902  limsupub  44905  limsuppnflem  44911  climinf3  44917  limsupmnflem  44921  climxrre  44951  liminfvalxr  44984  fperdvper  45120  sge0isum  45628  sge0gtfsumgt  45644  sge0seq  45647  nnfoctbdjlem  45656  meaiuninc3v  45685  omeiunltfirp  45720  hspdifhsp  45817  hspmbllem2  45828  pimdecfgtioo  45918  pimincfltioo  45919  preimageiingt  45921  preimaleiinlt  45922  smfid  45953  proththd  46767