Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Auxiliary axiom schemes (4 schemes)
Axiom scheme ax-12 (Substitution)
exlimimddOLD
Metamath Proof Explorer
Description: Obsolete version of exlimimdd as of 3-Sep-2023. (Contributed by ML , 17-Jul-2020) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Hypotheses
exlimdd.1
⊢ Ⅎ x φ
exlimdd.2
⊢ Ⅎ x χ
exlimdd.3
⊢ φ → ∃ x ψ
exlimimddOLD.4
⊢ φ → ψ → χ
Assertion
exlimimddOLD
⊢ φ → χ
Proof
Step
Hyp
Ref
Expression
1
exlimdd.1
⊢ Ⅎ x φ
2
exlimdd.2
⊢ Ⅎ x χ
3
exlimdd.3
⊢ φ → ∃ x ψ
4
exlimimddOLD.4
⊢ φ → ψ → χ
5
4
imp
⊢ φ ∧ ψ → χ
6
1 2 3 5
exlimdd
⊢ φ → χ