Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-frege8 Structured version   Visualization version   Unicode version

Axiom ax-frege8 36476
Description: Swap antecedents. If two conditions have a proposition as a consequence, their order is immaterial. Third axiom of Frege's 1879 work but identical to pm2.04 84 which can be proved from only ax-mp 5, ax-frege1 36457, and ax-frege2 36458. (Redundant) Axiom 8 of [Frege1879] p. 35. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
Assertion
Ref Expression
ax-frege8  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  ( ps  ->  ( ph  ->  ch ) ) )

Detailed syntax breakdown of Axiom ax-frege8
StepHypRef Expression
1 wph . 2  wff  ph
2 wps . . 3  wff  ps
3 wch . . 3  wff  ch
42, 3wi 4 . 2  wff  ( ps 
->  ch )
51, 3wi 4 . . 3  wff  ( ph  ->  ch )
62, 5wi 4 . 2  wff  ( ps 
->  ( ph  ->  ch ) )
71, 4, 6bj-0 31195 1  wff  ( (
ph  ->  ( ps  ->  ch ) )  ->  ( ps  ->  ( ph  ->  ch ) ) )
Colors of variables: wff setvar class
This axiom is referenced by:  frege26  36477  frege9  36479  frege12  36480  frege10  36487  frege17  36488  frege38  36508  frege53aid  36526  frege53a  36527  frege62a  36547  frege66a  36551  frege53b  36557  frege62b  36574  frege66b  36578  frege53c  36581  frege62c  36592  frege66c  36596  frege74  36604  frege84  36614  frege96  36626
  Copyright terms: Public domain W3C validator