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

Theorem baibr 915
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 914 . 2  |-  ( ps 
->  ( ph  <->  ch )
)
32bicomd 205 1  |-  ( ps 
->  ( ch  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189  df-an 373
This theorem is referenced by:  rbaibrOLD  919  pm5.44  922  exmoeu2  2326  ssnelpss  3829  brinxp  4897  copsex2ga  4946  canth  6249  riotaxfrd  6282  iscard  8409  kmlem14  8593  ltxrlt  9704  elioo5  11692  prmind2  14635  pcelnn  14819  isnirred  17928  isreg2  20393  comppfsc  20547  kqcldsat  20748  elmptrab  20842  itg2uba  22701  prmorcht  24105  adjeq  27588  lnopcnbd  27689  cvexchlem  28021  maprnin  28316  topfne  31010  ismblfin  31981  ftc1anclem5  32021  isdmn2  32288  cdlemefrs29pre00  33962  cdlemefrs29cpre1  33965  isdomn3  36081  elmapintab  36202  bits0ALTV  38808
  Copyright terms: Public domain W3C validator