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

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

Proof of Theorem bi2.04
StepHypRef Expression
1 pm2.04 78 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  ( ps  ->  ( ph  ->  ch ) ) )
2 pm2.04 78 . 2  |-  ( ( ps  ->  ( ph  ->  ch ) )  -> 
( ph  ->  ( ps 
->  ch ) ) )
31, 2impbii 182 1  |-  ( (
ph  ->  ( ps  ->  ch ) )  <->  ( ps  ->  ( ph  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  imim21b  358  pm4.87  570  imimorb  852  ax12b  1834  sbcom  1984  sbcom2  2077  r19.21t  2601  reu8  2929  ra5  3036  unissb  3817  reusv3  4500  fun11  5239  oeordi  6539  marypha1lem  7140  aceq1  7698  pwfseqlem3  8236  prime  10045  raluz2  10221  rlimresb  11990  isprm3  12715  isprm4  12716  acsfn  13509  pgpfac1  15263  pgpfac  15267  fbfinnfr  17484  wilthlem3  20256  isch3  21767  elat2  22866  pm10.541  26915  pm10.542  26916  isat3  28648  cdleme32fva  29777
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator