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  2297  ssnelpss  3651  brinxp  4899  copsex2ga  6367  canth  6498  riotaxfrd  6540  iscard  7818  kmlem14  7999  ltxrlt  9102  elioo5  10924  prmind2  13045  pcelnn  13198  isnirred  15760  isreg2  17395  kqcldsat  17718  elmptrab  17812  itg2uba  19588  prmorcht  20914  adjeq  23391  lnopcnbd  23492  cvexchlem  23824  ismblfin  26146  topfne  26260  comppfsc  26277  isdmn2  26555  isdomn3  27391  cdlemefrs29pre00  30877  cdlemefrs29cpre1  30880
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