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 37588
Description: Closed form of syl 17 with swapped antecedents. This proposition differs from frege5 37576 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 37576 . 2 ((𝜓𝜒) → ((𝜑𝜓) → (𝜑𝜒)))
2 ax-frege8 37585 . 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 37566  ax-frege2 37567  ax-frege8 37585
This theorem is referenced by:  frege11  37590  frege10  37596  frege19  37600  frege21  37603  frege37  37616  frege56aid  37646  frege56a  37647  frege61a  37655  frege56b  37674  frege61b  37682  frege56c  37695  frege61c  37700  frege117  37756  frege130  37769  frege132  37771
  Copyright terms: Public domain W3C validator