Metamath Proof Explorer

Theorem exlimddOLD

Description: Obsolete version of exlimdd as of 3-Sep-2023. (Contributed by Mario Carneiro, 9-Feb-2017) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses exlimdd.1 x φ
exlimdd.2 x χ
exlimdd.3 φ x ψ
exlimdd.4 φ ψ χ
Assertion exlimddOLD φ χ


Step Hyp Ref Expression
1 exlimdd.1 x φ
2 exlimdd.2 x χ
3 exlimdd.3 φ x ψ
4 exlimdd.4 φ ψ χ
5 4 ex φ ψ χ
6 1 2 5 exlimd φ x ψ χ
7 3 6 mpd φ χ