Theorem syl6an 1483

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 ⊢ (𝜑 → (𝜒 → 𝜏))

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-ia3 108

This theorem is used by:  mapxpen  7153  prarloclem5  7874  ltsopr  7970  suplocsrlem  8182  nominpos  9555  ublbneg  10030  wrdsymb0  11360  ccats1pfxeqrex  11510  absle  11879  rexanre  12010  rexico  12011  climshftlemg  12094  serf0  12144  dvds1lem  12595  dvds2lem  12596  lmconst  15454  addcncntoplem  15799  bj-indind  17175