Theorem 3jca 1132

Description: Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)

Hypotheses

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

Assertion

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

Proof of Theorem 3jca

Step	Hyp	Ref	Expression
1		3jca.1	. . 3 ⊢ (φ → ψ)
2		3jca.2	. . 3 ⊢ (φ → χ)
3		3jca.3	. . 3 ⊢ (φ → θ)
4	1, 2, 3	jca31 520	. 2 ⊢ (φ → ((ψ ∧ χ) ∧ θ))
5		df-3an 936	. 2 ⊢ ((ψ ∧ χ ∧ θ) ↔ ((ψ ∧ χ) ∧ θ))
6	4, 5	sylibr 203	1 ⊢ (φ → (ψ ∧ χ ∧ θ))

Syntax hints:   → wi 4   ∧ wa 358   ∧ w3a 934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

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

This theorem is referenced by:  3jcad  1133  mpbir3and  1135  syl3anbrc  1136  3anim123i  1137  syl3anc  1182  syl13anc  1184  syl31anc  1185  syl113anc  1194  syl131anc  1195  syl311anc  1196  syl33anc  1197  syl133anc  1205  syl313anc  1206  syl331anc  1207  syl333anc  1214  3jaob  1244  mp3and  1280  1cvsfin  4543