Metamath Proof Explorer


Theorem alimex

Description: An equivalence between an implication with a universally quantified consequent and an implication with an existentially quantified antecedent. An interesting case is when the same formula is substituted for both ph and ps , since then both implications express a type of nonfreeness. See also eximal . (Contributed by BJ, 12-May-2019)

Ref Expression
Assertion alimex φxψx¬ψ¬φ

Proof

Step Hyp Ref Expression
1 alex xψ¬x¬ψ
2 1 imbi2i φxψφ¬x¬ψ
3 con2b φ¬x¬ψx¬ψ¬φ
4 2 3 bitri φxψx¬ψ¬φ