Metamath Proof Explorer

Theorem frege64b

Description: Lemma for frege65b . Proposition 64 of Frege1879 p. 53. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege64b ( ( [ 𝑥 / 𝑦 ] 𝜑 → [ 𝑧 / 𝑦 ] 𝜓 ) → ( ∀ 𝑦 ( 𝜓 → 𝜒 ) → ( [ 𝑥 / 𝑦 ] 𝜑 → [ 𝑧 / 𝑦 ] 𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 frege62b ⊢ ( [ 𝑧 / 𝑦 ] 𝜓 → ( ∀ 𝑦 ( 𝜓 → 𝜒 ) → [ 𝑧 / 𝑦 ] 𝜒 ) )
2 frege18 ⊢ ( ( [ 𝑧 / 𝑦 ] 𝜓 → ( ∀ 𝑦 ( 𝜓 → 𝜒 ) → [ 𝑧 / 𝑦 ] 𝜒 ) ) → ( ( [ 𝑥 / 𝑦 ] 𝜑 → [ 𝑧 / 𝑦 ] 𝜓 ) → ( ∀ 𝑦 ( 𝜓 → 𝜒 ) → ( [ 𝑥 / 𝑦 ] 𝜑 → [ 𝑧 / 𝑦 ] 𝜒 ) ) ) )
3 1 2 ax-mp ⊢ ( ( [ 𝑥 / 𝑦 ] 𝜑 → [ 𝑧 / 𝑦 ] 𝜓 ) → ( ∀ 𝑦 ( 𝜓 → 𝜒 ) → ( [ 𝑥 / 𝑦 ] 𝜑 → [ 𝑧 / 𝑦 ] 𝜒 ) ) )