Theorem ad4ant13 749

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 483	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 717	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ad5ant14  756  ad5ant24  759  fntpb  6974  peano5  7607  f1o2ndf1  7820  cantnfle  9136  cantnflem1c  9152  ttukeylem5  9937  rlimsqzlem  15007  dvdslcmf  15977  poslubmo  17758  posglbmo  17759  smndex1mgm  18074  isgrpinv  18158  ghmgrp  18225  dprdfcntz  19139  cply1coe0bi  20470  isnrm3  21969  cnextcn  22677  ustexsym  22826  ustex2sym  22827  ustex3sym  22828  trust  22840  fmucnd  22903  trcfilu  22905  metust  23170  cxpmul2z  25276  umgrres1lem  27094  upgrres1  27097  friendshipgt3  28179  ccatf1  30627  cyc3evpm  30794  txomap  31100  repr0  31884  breprexplemc  31905  hgt750lemb  31929  satffunlem1lem2  32652  satffunlem2lem2  32655  lindsadd  34887  matunitlindflem1  34890  mapss2  41475  supxrge  41613  xrlexaddrp  41627  infxr  41642  infleinf  41647  unb2ltle  41696  supminfxr  41747  limsuppnfdlem  41989  limsupub  41992  limsuppnflem  41998  climinf3  42004  limsupmnflem  42008  climxrre  42038  liminfvalxr  42071  fperdvper  42210  sge0isum  42716  sge0gtfsumgt  42732  sge0seq  42735  nnfoctbdjlem  42744  meaiuninc3v  42773  omeiunltfirp  42808  hspdifhsp  42905  hspmbllem2  42916  pimdecfgtioo  43002  pimincfltioo  43003  preimageiingt  43005  preimaleiinlt  43006  smfid  43036  proththd  43786