MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bi2.04 Structured version   Unicode version

Theorem bi2.04 359
Description: Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 11-May-1993.)
Assertion
Ref Expression
bi2.04  |-  ( (
ph  ->  ( ps  ->  ch ) )  <->  ( ps  ->  ( ph  ->  ch ) ) )

Proof of Theorem bi2.04
StepHypRef Expression
1 pm2.04 82 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  ( ps  ->  ( ph  ->  ch ) ) )
2 pm2.04 82 . 2  |-  ( ( ps  ->  ( ph  ->  ch ) )  -> 
( ph  ->  ( ps 
->  ch ) ) )
31, 2impbii 188 1  |-  ( (
ph  ->  ( ps  ->  ch ) )  <->  ( ps  ->  ( ph  ->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  imim21b  365  pm4.87  582  imimorb  875  r19.21t  2793  r19.21tOLD  2794  r19.21v  2801  reu8  3237  ra4vOLD  3355  ra4OLD  3357  unissb  4211  reusv3  4590  fun11  5578  oeordi  7176  marypha1lem  7830  aceq1  8433  pwfseqlem3  8971  prime  10882  raluz2  11072  rlimresb  13413  isprm3  14251  isprm4  14252  acsfn  15089  pgpfac1  17267  pgpfac  17271  fbfinnfr  20450  wilthlem3  23484  isch3  26301  elat2  27400  pm10.541  31480  pm10.542  31481  isat3  35484  cdleme32fva  36615
  Copyright terms: Public domain W3C validator