Theorem sylanl1 680

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 590	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))
3		sylanl1.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylan 487	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  adantlll  750  adantllr  751  isocnv  6480  odi  7546  oeoelem  7565  mapxpen  8011  xadddilem  11996  pcqmul  15396  infpnlem1  15452  chpdmat  20465  neitr  20794  hausflimi  21594  nmoix  22343  nmoleub  22345  metdsre  22464  pthdepisspth  26104  extwwlkfab  26617  sspph  27094  unoplin  28163  hmoplin  28185  chirredlem1  28633  mdsymlem2  28647  foresf1o  28727  ordtconlem1  29298  isbasisrelowllem1  32379  isbasisrelowllem2  32380  lindsdom  32573  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem25  32604  poimirlem29  32608  heicant  32614  cnambfre  32628  itg2addnclem  32631  ftc1anclem5  32659  ftc1anc  32663  rrnequiv  32804  isfldidl  33037  ispridlc  33039  supxrgelem  38494  usgr2edg1  40439  crctcsh1wlkn0  41024  reccot  42298  rectan  42299