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 38600
Description: Closed form of syl 17 with swapped antecedents. This proposition differs from frege5 38588 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 38588 . 2 ((𝜓𝜒) → ((𝜑𝜓) → (𝜑𝜒)))
2 ax-frege8 38597 . 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 38578  ax-frege2 38579  ax-frege8 38597
This theorem is referenced by:  frege11  38602  frege10  38608  frege19  38612  frege21  38615  frege37  38628  frege56aid  38658  frege56a  38659  frege61a  38667  frege56b  38686  frege61b  38694  frege56c  38707  frege61c  38712  frege117  38768  frege130  38781  frege132  38783
  Copyright terms: Public domain W3C validator