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

Metamath Proof Explorer

Theorem mpbi

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 11-May-1993)

Ref Expression
Hypotheses mpbi.min ⊢ φ
mpbi.maj ⊢ φ ↔ ψ
Assertion mpbi ⊢ ψ

Proof

Step Hyp Ref Expression
1 mpbi.min ⊢ φ
2 mpbi.maj ⊢ φ ↔ ψ
3 2 biimpi ⊢ φ → ψ
4 1 3 ax-mp ⊢ ψ