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

Metamath Proof Explorer

Theorem imdistan

Description: Distribution of implication with conjunction. (Contributed by NM, 31-May-1999) (Proof shortened by Wolf Lammen, 6-Dec-2012)

Ref Expression
Assertion imdistan ⊢ φ → ψ → χ ↔ φ ∧ ψ → φ ∧ χ

Proof

Step Hyp Ref Expression
1 pm5.42 ⊢ φ → ψ → χ ↔ φ → ψ → φ ∧ χ
2 impexp ⊢ φ ∧ ψ → φ ∧ χ ↔ φ → ψ → φ ∧ χ
3 1 2 bitr4i ⊢ φ → ψ → χ ↔ φ ∧ ψ → φ ∧ χ