Metamath Proof Explorer


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 ( ∀ 𝑥 ( 𝜑 → ( 𝜓𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜓 → ( [ 𝐴 / 𝑥 ] 𝜑[ 𝐴 / 𝑥 ] 𝜒 ) ) )