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

Theorem baibr 902
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 901 . 2  |-  ( ps 
->  ( ph  <->  ch )
)
32bicomd 201 1  |-  ( ps 
->  ( ch  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  rbaibrOLD  906  pm5.44  909  exmoeu2  2306  ssnelpss  3890  brinxp  5061  copsex2ga  5112  canth  6240  riotaxfrd  6274  iscard  8352  kmlem14  8539  ltxrlt  9651  elioo5  11578  prmind2  14083  pcelnn  14248  isnirred  17133  isreg2  19644  kqcldsat  19969  elmptrab  20063  itg2uba  21885  prmorcht  23180  adjeq  26530  lnopcnbd  26631  cvexchlem  26963  maprnin  27226  ismblfin  29632  ftc1anclem5  29671  topfne  29762  comppfsc  29779  isdmn2  30055  isdomn3  30769  cdlemefrs29pre00  35191  cdlemefrs29cpre1  35194
  Copyright terms: Public domain W3C validator