MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-2 Unicode version

Axiom ax-2 6
Description: Axiom Frege. Axiom A2 of [Margaris] p. 49. One of the 3 axioms of propositional calculus. It "distributes" an antecedent over two consequents. This axiom was part of Frege's original system and is known as Frege in the literature. It is also proved as Theorem *2.77 of [WhiteheadRussell] p. 108. The other direction of this axiom also turns out to be true, as demonstrated by pm5.41 354. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ax-2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  ->  ps )  ->  ( ph  ->  ch ) ) )

Detailed syntax breakdown of Axiom ax-2
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . . 4  wff  ps
3 wch . . . 4  wff  ch
42, 3wi 4 . . 3  wff  ( ps 
->  ch )
51, 4wi 4 . 2  wff  ( ph  ->  ( ps  ->  ch ) )
61, 2wi 4 . . 3  wff  ( ph  ->  ps )
71, 3wi 4 . . 3  wff  ( ph  ->  ch )
86, 7wi 4 . 2  wff  ( (
ph  ->  ps )  -> 
( ph  ->  ch )
)
95, 8wi 4 1  wff  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  ->  ps )  ->  ( ph  ->  ch ) ) )
Colors of variables: wff set class
This axiom is referenced by:  a2i  13  id1  21  a2d  24  dfbi1gb  186  imdi  353  sbi1  2112  ralim  2737  difin0ss  3654  sbi1NEW7  29267
  Copyright terms: Public domain W3C validator