Metamath Proof Explorer


Theorem frege59c

Description: A kind of Aristotelian inference. Proposition 59 of Frege1879 p. 51.

Note: in the Bauer-Meenfelberg translation published in van Heijenoort's collectionFrom Frege to Goedel, this proof has the frege12 incorrectly referenced where frege30 is in the original. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege59c.a 𝐴𝐵
Assertion frege59c ( [ 𝐴 / 𝑥 ] 𝜑 → ( ¬ [ 𝐴 / 𝑥 ] 𝜓 → ¬ ∀ 𝑥 ( 𝜑𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 frege59c.a 𝐴𝐵
2 1 frege58c ( ∀ 𝑥 ( 𝜑𝜓 ) → [ 𝐴 / 𝑥 ] ( 𝜑𝜓 ) )
3 sbcim1 ( [ 𝐴 / 𝑥 ] ( 𝜑𝜓 ) → ( [ 𝐴 / 𝑥 ] 𝜑[ 𝐴 / 𝑥 ] 𝜓 ) )
4 2 3 syl ( ∀ 𝑥 ( 𝜑𝜓 ) → ( [ 𝐴 / 𝑥 ] 𝜑[ 𝐴 / 𝑥 ] 𝜓 ) )
5 frege30 ( ( ∀ 𝑥 ( 𝜑𝜓 ) → ( [ 𝐴 / 𝑥 ] 𝜑[ 𝐴 / 𝑥 ] 𝜓 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → ( ¬ [ 𝐴 / 𝑥 ] 𝜓 → ¬ ∀ 𝑥 ( 𝜑𝜓 ) ) ) )
6 4 5 ax-mp ( [ 𝐴 / 𝑥 ] 𝜑 → ( ¬ [ 𝐴 / 𝑥 ] 𝜓 → ¬ ∀ 𝑥 ( 𝜑𝜓 ) ) )