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 38933
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 38923 . 2 ((𝜑𝜓) → (𝜒 → (𝜑𝜓)))
2 frege4 38932 . 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 38923  ax-frege2 38924
This theorem is referenced by:  rp-frege25  38938  frege6  38939  frege7  38941  frege9  38945  frege12  38946  frege16  38949  frege25  38950  frege18  38951  frege22  38952  frege14  38956  frege29  38964  frege34  38970  frege45  38982  frege80  39076  frege90  39086
  Copyright terms: Public domain W3C validator