Theorem sylanl1 406

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  adantlll  484  adantllr  485  adantl3r  516  isocnv  6020  mapxpen  7154  nqnq0pi  7812  nqpnq0nq  7827  addnqprl  7903  addnqpru  7904  pcqmul  13111  infpnlem1  13167  setsn0fun  13447  dvmptfsum  15984  chtqub  16329  usgr2edg  16687  usgr2edg1  16689