MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bi2.04 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

Proof of Theorem bi2.04
StepHypRef Expression
1 pm2.04 82 . 2
2 pm2.04 82 . 2
31, 2impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  imim21b  367  pm4.87  584  imimorb  877  r19.21t  2854  r19.21tOLD  2855  r19.21v  2862  reu8  3295  ra4vOLD  3424  ra4OLD  3426  unissb  4281  reusv3  4660  fun11  5658  oeordi  7255  marypha1lem  7913  aceq1  8519  pwfseqlem3  9059  prime  10968  raluz2  11159  rlimresb  13388  isprm3  14226  isprm4  14227  acsfn  15056  pgpfac1  17131  pgpfac  17135  fbfinnfr  20342  wilthlem3  23344  isch3  26159  elat2  27259  pm10.541  31272  pm10.542  31273  isat3  35032  cdleme32fva  36163
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
  Copyright terms: Public domain W3C validator