Theorem sylanl1 693

Description: A syllogism inference. (Contributed by NM, 10-Mar-2005.)

Hypotheses

Ref	Expression
sylanl1.1	⊢ (𝜑 → 𝜓)
sylanl1.2	⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
sylanl1	⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem sylanl1

Step	Hyp	Ref	Expression
1		sylanl1.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	anim1i 627	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))
3		sylanl1.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylan 592	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:  adantlll  731  adantllr  732  adantl3r  763  isocnv  7332  f1iun  7943  odi  8566  oeoelem  8586  mapxpen  9133  xadddilem  13330  hashgt23el  14472  pcqmul  16923  infpnlem1  16980  setsn0fun  17243  chpdmat  23013  neitr  23352  hausflimi  24152  nmoix  24901  nmoleub  24903  metdsre  25026  bncssbn  25548  usgr2edg  29575  usgr2edg1  29577  crctcshwlkn0  30185  unoplin  32287  hmoplin  32309  chirredlem1  32757  mdsymlem2  32771  foresf1o  32865  zarcls1  34272  ordtconnlem1  34327  signstfvn  34969  isbasisrelowllem1  38033  isbasisrelowllem2  38034  pibt2  38095  lindsadd  38296  lindsdom  38297  matunitlindflem1  38299  matunitlindflem2  38300  poimirlem25  38328  poimirlem29  38332  heicant  38338  cnambfre  38351  itg2addnclem  38354  ftc1anclem5  38380  ftc1anc  38384  rrnequiv  38518  isfldidl  38751  ispridlc  38753  supxrgelem  46085  supminfxr  46210  uhgrimisgrgric  48728  cycl3grtri  48744  gpg5nbgrvtx03star  48877  gpg5nbgr3star  48878  itcovalt2lem2  49488  reccot  50568  rectan  50569