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 42853
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 42843 . 2 ((𝜑𝜓) → (𝜒 → (𝜑𝜓)))
2 frege4 42852 . 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 42843  ax-frege2 42844
This theorem is referenced by:  rp-frege25  42858  frege6  42859  frege7  42861  frege9  42865  frege12  42866  frege16  42869  frege25  42870  frege18  42871  frege22  42872  frege14  42876  frege29  42884  frege34  42890  frege45  42902  frege80  42996  frege90  43006
  Copyright terms: Public domain W3C validator