Theorem syl6an 1479

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  7100  prarloclem5  7811  ltsopr  7907  suplocsrlem  8119  nominpos  9472  ublbneg  9941  wrdsymb0  11250  ccats1pfxeqrex  11400  absle  11767  rexanre  11898  rexico  11899  climshftlemg  11980  serf0  12030  dvds1lem  12481  dvds2lem  12482  lmconst  15068  addcncntoplem  15413  bj-indind  16689