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

Theorem frege5 42160
Description: A closed form of syl 17. Identical to imim2 58. Theorem *2.05 of [WhiteheadRussell] p. 100. Proposition 5 of [Frege1879] p. 32. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
Assertion
Ref Expression
frege5 ((𝜑𝜓) → ((𝜒𝜑) → (𝜒𝜓)))

Proof of Theorem frege5
StepHypRef Expression
1 ax-frege1 42150 . 2 ((𝜑𝜓) → (𝜒 → (𝜑𝜓)))
2 frege4 42159 . 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
This theorem is referenced by:  rp-frege25  42165  frege6  42166  frege7  42168  frege9  42172  frege12  42173  frege16  42176  frege25  42177  frege18  42178  frege22  42179  frege14  42183  frege29  42191  frege34  42197  frege45  42209  frege80  42303  frege90  42313
  Copyright terms: Public domain W3C validator