Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frege9 Structured version   Visualization version   GIF version

Theorem frege9 43825
Description: Closed form of syl 17 with swapped antecedents. This proposition differs from frege5 43813 only in an unessential way. Identical to imim1 83. Proposition 9 of [Frege1879] p. 35. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
Assertion
Ref Expression
frege9 ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))

Proof of Theorem frege9
StepHypRef Expression
1 frege5 43813 . 2 ((𝜓𝜒) → ((𝜑𝜓) → (𝜑𝜒)))
2 ax-frege8 43822 . 2 (((𝜓𝜒) → ((𝜑𝜓) → (𝜑𝜒))) → ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒))))
31, 2ax-mp 5 1 ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-frege1 43803  ax-frege2 43804  ax-frege8 43822
This theorem is referenced by:  frege11  43827  frege10  43833  frege19  43837  frege21  43840  frege37  43853  frege56aid  43883  frege56a  43884  frege61a  43892  frege56b  43911  frege61b  43919  frege56c  43932  frege61c  43937  frege117  43993  frege130  44006  frege132  44008
  Copyright terms: Public domain W3C validator