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 40007
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 39997 . 2 ((𝜑𝜓) → (𝜒 → (𝜑𝜓)))
2 frege4 40006 . 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 39997  ax-frege2 39998
This theorem is referenced by:  rp-frege25  40012  frege6  40013  frege7  40015  frege9  40019  frege12  40020  frege16  40023  frege25  40024  frege18  40025  frege22  40026  frege14  40030  frege29  40038  frege34  40044  frege45  40056  frege80  40150  frege90  40160
  Copyright terms: Public domain W3C validator