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  2199  ssnelpss  3530  brinxp  4768  copsex2ga  6197  canth  6310  riotaxfrd  6352  iscard  7624  kmlem14  7805  ltxrlt  8909  elioo5  10724  prmind2  12785  pcelnn  12938  isnirred  15498  isreg2  17121  kqcldsat  17440  elmptrab  17538  itg2uba  19114  prmorcht  20432  adjeq  22531  lnopcnbd  22632  cvexchlem  22964  topfne  26393  comppfsc  26410  isdmn2  26783  isdomn3  27626  cdlemefrs29pre00  31206  cdlemefrs29cpre1  31209
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