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

Theorem bi2.04 361
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  367  pm4.87  584  imimorb  872  sbcom2OLD  2161  r19.21t  2907  reu8  3262  ra4  3390  unissb  4232  reusv3  4609  fun11  5592  oeordi  7137  marypha1lem  7795  aceq1  8399  pwfseqlem3  8939  prime  10834  raluz2  11016  rlimresb  13162  isprm3  13891  isprm4  13892  acsfn  14717  pgpfac1  16704  pgpfac  16708  fbfinnfr  19547  wilthlem3  22542  isch3  24797  elat2  25897  pm10.541  29768  pm10.542  29769  isat3  33291  cdleme32fva  34420
  Copyright terms: Public domain W3C validator