Theorem frege60b

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

	Ref	Expression
Assertion	frege60b	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝑦 / 𝑥 ] 𝜓 → ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-frege58b	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → [ 𝑦 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) )
2		sbim	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] ( 𝜓 → 𝜒 ) ) )
3		sbim	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜓 → [ 𝑦 / 𝑥 ] 𝜒 ) )
4	3	imbi2i	⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜓 → [ 𝑦 / 𝑥 ] 𝜒 ) ) )
5	2 4	bitri	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜓 → [ 𝑦 / 𝑥 ] 𝜒 ) ) )
6	1 5	sylib	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝑦 / 𝑥 ] 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜓 → [ 𝑦 / 𝑥 ] 𝜒 ) ) )
7		frege12	⊢ ( ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝑦 / 𝑥 ] 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜓 → [ 𝑦 / 𝑥 ] 𝜒 ) ) ) → ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝑦 / 𝑥 ] 𝜓 → ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜒 ) ) ) )
8	6 7	ax-mp	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝑦 / 𝑥 ] 𝜓 → ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜒 ) ) )