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

Metamath Proof Explorer

Theorem bnj951

Description: /\ -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 bnj951.1 ⊢ ( 𝜏 → 𝜑 )
2 bnj951.2 ⊢ ( 𝜏 → 𝜓 )
3 bnj951.3 ⊢ ( 𝜏 → 𝜒 )
4 bnj951.4 ⊢ ( 𝜏 → 𝜃 )
5 1 2 3 3jca ⊢ ( 𝜏 → ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) )
6 df-bnj17 ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )
7 5 4 6 sylanbrc ⊢ ( 𝜏 → ( 𝜑 ∧ 𝜓 ∧ 𝜒 ∧ 𝜃 ) )