Theorem frege65c

Description: A kind of Aristotelian inference. This judgement replaces the mode of inference barbara when the minor premise has a general context. Proposition 65 of Frege1879 p. 53. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	frege59c.a	⊢ 𝐴 ∈ 𝐵
Assertion	frege65c	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 ( 𝜓 → 𝜒 ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		frege59c.a	⊢ 𝐴 ∈ 𝐵
2		sbcim1	⊢ ( [ 𝐴 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜓 ) )
3	1	frege64c	⊢ ( ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜓 ) → ( ∀ 𝑥 ( 𝜓 → 𝜒 ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜒 ) ) )
4	2 3	syl	⊢ ( [ 𝐴 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 ( 𝜓 → 𝜒 ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜒 ) ) )
5	1	frege61c	⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 ( 𝜓 → 𝜒 ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 ( 𝜓 → 𝜒 ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) )
6	4 5	ax-mp	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 ( 𝜓 → 𝜒 ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜒 ) ) )