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

Metamath Proof Explorer

Theorem mpbir

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992)

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

Proof

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