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

Metamath Proof Explorer

Theorem bnj240

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

Ref Expression
Hypotheses bnj240.1 ⊢ ( 𝜓 → 𝜓′ )
bnj240.2 ⊢ ( 𝜒 → 𝜒′ )
Assertion bnj240 ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → ( 𝜓′ ∧ 𝜒′ ) )

Proof

Step Hyp Ref Expression
1 bnj240.1 ⊢ ( 𝜓 → 𝜓′ )
2 bnj240.2 ⊢ ( 𝜒 → 𝜒′ )
3 1 3ad2ant1 ⊢ ( ( 𝜓 ∧ 𝜒 ∧ 𝜑 ) → 𝜓′ )
4 2 3ad2ant2 ⊢ ( ( 𝜓 ∧ 𝜒 ∧ 𝜑 ) → 𝜒′ )
5 3 4 jca ⊢ ( ( 𝜓 ∧ 𝜒 ∧ 𝜑 ) → ( 𝜓′ ∧ 𝜒′ ) )
6 5 3comr ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → ( 𝜓′ ∧ 𝜒′ ) )