Theorem sylanl1 683

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 591	. 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 197  df-an 385

This theorem is referenced by:  adantlll  754  adantllr  755  isocnv  6620  odi  7704  oeoelem  7723  mapxpen  8167  xadddilem  12162  pcqmul  15605  infpnlem1  15661  setsn0fun  15942  chpdmat  20694  neitr  21032  hausflimi  21831  nmoix  22580  nmoleub  22582  metdsre  22703  usgr2edg1  26149  crctcshwlkn0  26769  sspph  27838  unoplin  28907  hmoplin  28929  chirredlem1  29377  mdsymlem2  29391  foresf1o  29469  ordtconnlem1  30098  isbasisrelowllem1  33333  isbasisrelowllem2  33334  lindsdom  33533  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem25  33564  poimirlem29  33568  heicant  33574  cnambfre  33588  itg2addnclem  33591  ftc1anclem5  33619  ftc1anc  33623  rrnequiv  33764  isfldidl  33997  ispridlc  33999  supxrgelem  39866  supminfxr  40007  reccot  42827  rectan  42828