Metamath Proof Explorer


Theorem bj-mt2bi

Description: Version of mt2 where the major premise is a biconditional. Another proof is also possible via con2bii and mpbi . The current mt2bi should be relabeled, maybe to imfal. (Contributed by BJ, 5-Oct-2024)

Ref Expression
Hypotheses bj-mt2bi.min φ
bj-mt2bi.maj ψ ¬ φ
Assertion bj-mt2bi ¬ ψ

Proof

Step Hyp Ref Expression
1 bj-mt2bi.min φ
2 bj-mt2bi.maj ψ ¬ φ
3 2 biimpi ψ ¬ φ
4 1 3 mt2 ¬ ψ