Theorem sylanl1 682

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

Syntax hints:   → wi 4   ∧ wa 384

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 386

This theorem is referenced by:  adantlll  754  adantllr  755  isocnv  6580  odi  7659  oeoelem  7678  mapxpen  8126  xadddilem  12124  pcqmul  15558  infpnlem1  15614  setsn0fun  15895  chpdmat  20646  neitr  20984  hausflimi  21784  nmoix  22533  nmoleub  22535  metdsre  22656  usgr2edg1  26104  crctcshwlkn0  26713  sspph  27710  unoplin  28779  hmoplin  28801  chirredlem1  29249  mdsymlem2  29263  foresf1o  29343  ordtconnlem1  29970  isbasisrelowllem1  33203  isbasisrelowllem2  33204  lindsdom  33403  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem25  33434  poimirlem29  33438  heicant  33444  cnambfre  33458  itg2addnclem  33461  ftc1anclem5  33489  ftc1anc  33493  rrnequiv  33634  isfldidl  33867  ispridlc  33869  supxrgelem  39553  supminfxr  39694  reccot  42499  rectan  42500