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

Theorem baibr 873
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 872 . 2  |-  ( ps 
->  ( ph  <->  ch )
)
32bicomd 193 1  |-  ( ps 
->  ( ch  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  rbaibr  875  pm5.44  878  exmoeu2  2323  ssnelpss  3683  brinxp  4932  copsex2ga  6400  canth  6531  riotaxfrd  6573  iscard  7854  kmlem14  8035  ltxrlt  9138  elioo5  10960  prmind2  13082  pcelnn  13235  isnirred  15797  isreg2  17433  kqcldsat  17757  elmptrab  17851  itg2uba  19627  prmorcht  20953  adjeq  23430  lnopcnbd  23531  cvexchlem  23863  ismblfin  26237  topfne  26351  comppfsc  26368  isdmn2  26646  isdomn3  27481  cdlemefrs29pre00  31119  cdlemefrs29cpre1  31122
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 178  df-an 361
  Copyright terms: Public domain W3C validator