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

Theorem baibr 872
Description: Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
Hypothesis
Ref Expression
baib.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
baibr  |-  ( ps 
->  ( ch  <->  ph ) )

Proof of Theorem baibr
StepHypRef Expression
1 baib.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
21baib 871 . 2  |-  ( ps 
->  ( ph  <->  ch )
)
32bicomd 192 1  |-  ( ps 
->  ( ch  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  rbaibr  874  pm5.44  877  exmoeu2  2186  ssnelpss  3517  brinxp  4752  copsex2ga  6181  canth  6294  riotaxfrd  6336  iscard  7608  kmlem14  7789  ltxrlt  8893  elioo5  10708  prmind2  12769  pcelnn  12922  isnirred  15482  isreg2  17105  kqcldsat  17424  elmptrab  17522  itg2uba  19098  prmorcht  20416  adjeq  22515  lnopcnbd  22616  cvexchlem  22948  topfne  26290  comppfsc  26307  isdmn2  26680  isdomn3  27523  cdlemefrs29pre00  30584  cdlemefrs29cpre1  30587
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator