MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  baibr 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  2283  ssnelpss  3636  brinxp  4882  copsex2ga  6349  canth  6477  riotaxfrd  6519  iscard  7797  kmlem14  7978  ltxrlt  9081  elioo5  10902  prmind2  13019  pcelnn  13172  isnirred  15734  isreg2  17365  kqcldsat  17688  elmptrab  17782  itg2uba  19504  prmorcht  20830  adjeq  23288  lnopcnbd  23389  cvexchlem  23721  topfne  26063  comppfsc  26080  isdmn2  26358  isdomn3  27194  cdlemefrs29pre00  30511  cdlemefrs29cpre1  30514
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