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 40025
Description: Closed form of syl 17 with swapped antecedents. This proposition differs from frege5 40013 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 40013 . 2 ((𝜓𝜒) → ((𝜑𝜓) → (𝜑𝜒)))
2 ax-frege8 40022 . 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 40003  ax-frege2 40004  ax-frege8 40022
This theorem is referenced by:  frege11  40027  frege10  40033  frege19  40037  frege21  40040  frege37  40053  frege56aid  40083  frege56a  40084  frege61a  40092  frege56b  40111  frege61b  40119  frege56c  40132  frege61c  40137  frege117  40193  frege130  40206  frege132  40208
  Copyright terms: Public domain W3C validator