Theorem syl6an 1445

Description: A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.)

Hypotheses

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

Assertion

Ref	Expression
syl6an	⊢ (𝜑 → (𝜒 → 𝜏))

Proof of Theorem syl6an

Step	Hyp	Ref	Expression
1		syl6an.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜃))
2		syl6an.1	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	jctild 316	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 ∧ 𝜃)))
4		syl6an.3	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜏)
5	3, 4	syl6 33	1 ⊢ (𝜑 → (𝜒 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mapxpen  6910  prarloclem5  7569  ltsopr  7665  suplocsrlem  7877  nominpos  9231  ublbneg  9689  wrdsymb0  10969  absle  11256  rexanre  11387  rexico  11388  climshftlemg  11469  serf0  11519  dvds1lem  11969  dvds2lem  11970  lmconst  14462  addcncntoplem  14807  bj-indind  15588