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 42172
Description: Closed form of syl 17 with swapped antecedents. This proposition differs from frege5 42160 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 42160 . 2 ((𝜓𝜒) → ((𝜑𝜓) → (𝜑𝜒)))
2 ax-frege8 42169 . 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 42150  ax-frege2 42151  ax-frege8 42169
This theorem is referenced by:  frege11  42174  frege10  42180  frege19  42184  frege21  42187  frege37  42200  frege56aid  42230  frege56a  42231  frege61a  42239  frege56b  42258  frege61b  42266  frege56c  42279  frege61c  42284  frege117  42340  frege130  42353  frege132  42355
  Copyright terms: Public domain W3C validator