Theorem 3jcad 1133

Description: Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.)

Hypotheses

Ref	Expression
3jcad.1	⊢ (φ → (ψ → χ))
3jcad.2	⊢ (φ → (ψ → θ))
3jcad.3	⊢ (φ → (ψ → τ))

Assertion

Ref	Expression
3jcad	⊢ (φ → (ψ → (χ ∧ θ ∧ τ)))

Proof of Theorem 3jcad

Step	Hyp	Ref	Expression
1		3jcad.1	. . . 4 ⊢ (φ → (ψ → χ))
2	1	imp 418	. . 3 ⊢ ((φ ∧ ψ) → χ)
3		3jcad.2	. . . 4 ⊢ (φ → (ψ → θ))
4	3	imp 418	. . 3 ⊢ ((φ ∧ ψ) → θ)
5		3jcad.3	. . . 4 ⊢ (φ → (ψ → τ))
6	5	imp 418	. . 3 ⊢ ((φ ∧ ψ) → τ)
7	2, 4, 6	3jca 1132	. 2 ⊢ ((φ ∧ ψ) → (χ ∧ θ ∧ τ))
8	7	ex 423	1 ⊢ (φ → (ψ → (χ ∧ θ ∧ τ)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 358   ∧ w3a 934

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177  df-an 360  df-3an 936

This theorem is used by: (None)