Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Auxiliary axiom schemes (4 schemes)
Axiom scheme ax-12 (Substitution)
sblim
Metamath Proof Explorer
Description: Substitution in an implication with a variable not free in the
consequent affects only the antecedent. (Contributed by NM , 14-Nov-2013) (Revised by Mario Carneiro , 4-Oct-2016)
Ref
Expression
Hypothesis
sblim.1
⊢ Ⅎ 𝑥 𝜓
Assertion
sblim
⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → 𝜓 ) )
Proof
Step
Hyp
Ref
Expression
1
sblim.1
⊢ Ⅎ 𝑥 𝜓
2
sbim
⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
3
1
sbf
⊢ ( [ 𝑦 / 𝑥 ] 𝜓 ↔ 𝜓 )
4
3
imbi2i
⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → 𝜓 ) )
5
2 4
bitri
⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → 𝜓 ) )