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

Metamath Proof Explorer

Theorem pm4.38

Description: Theorem *4.38 of WhiteheadRussell p. 118. (Contributed by NM, 3-Jan-2005)

Ref Expression
Assertion pm4.38 ⊢ φ ↔ χ ∧ ψ ↔ θ → φ ∧ ψ ↔ χ ∧ θ

Proof

Step Hyp Ref Expression
1 simpl ⊢ φ ↔ χ ∧ ψ ↔ θ → φ ↔ χ
2 simpr ⊢ φ ↔ χ ∧ ψ ↔ θ → ψ ↔ θ
3 1 2 anbi12d ⊢ φ ↔ χ ∧ ψ ↔ θ → φ ∧ ψ ↔ χ ∧ θ