This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3jca

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

Ref Expression
Hypotheses 3jca.1 ⊢ ( 𝜑 → 𝜓 )
3jca.2 ⊢ ( 𝜑 → 𝜒 )
3jca.3 ⊢ ( 𝜑 → 𝜃 )
Assertion 3jca ( 𝜑 → ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) )

Proof

Step Hyp Ref Expression
1 3jca.1 ⊢ ( 𝜑 → 𝜓 )
2 3jca.2 ⊢ ( 𝜑 → 𝜒 )
3 3jca.3 ⊢ ( 𝜑 → 𝜃 )
4 1 2 3 jca31 ⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )
5 df-3an ⊢ ( ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )
6 4 5 sylibr ⊢ ( 𝜑 → ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) )