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

Metamath Proof Explorer

Theorem ibar

Description: Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995)

Ref Expression
Assertion ibar ⊢ φ → ψ ↔ φ ∧ ψ

Proof

Step Hyp Ref Expression
1 iba ⊢ φ → ψ ↔ ψ ∧ φ
2 1 biancomd ⊢ φ → ψ ↔ φ ∧ ψ