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 ⊢ τ → φ ∧ ψ ∧ χ ∧ θ