Theorem frege60c

Description: Swap antecedents of frege58c . Proposition 60 of Frege1879 p. 52. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

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

Proof

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