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  6918  prarloclem5  7586  ltsopr  7682  suplocsrlem  7894  nominpos  9248  ublbneg  9706  wrdsymb0  10986  absle  11273  rexanre  11404  rexico  11405  climshftlemg  11486  serf0  11536  dvds1lem  11986  dvds2lem  11987  lmconst  14538  addcncntoplem  14883  bj-indind  15664