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 40954
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 40944 . 2 ((𝜑𝜓) → (𝜒 → (𝜑𝜓)))
2 frege4 40953 . 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 40944  ax-frege2 40945
This theorem is referenced by:  rp-frege25  40959  frege6  40960  frege7  40962  frege9  40966  frege12  40967  frege16  40970  frege25  40971  frege18  40972  frege22  40973  frege14  40977  frege29  40985  frege34  40991  frege45  41003  frege80  41097  frege90  41107
  Copyright terms: Public domain W3C validator