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 367
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 369
This theorem is referenced by:  rbaibrOLD  906  pm5.44  909  exmoeu2  2313  ssnelpss  3878  brinxp  5051  copsex2ga  5102  canth  6229  riotaxfrd  6262  iscard  8347  kmlem14  8534  ltxrlt  9644  elioo5  11585  prmind2  14315  pcelnn  14480  isnirred  17547  isreg2  20048  comppfsc  20202  kqcldsat  20403  elmptrab  20497  itg2uba  22319  prmorcht  23653  adjeq  27055  lnopcnbd  27156  cvexchlem  27488  maprnin  27788  ismblfin  30298  ftc1anclem5  30337  topfne  30415  isdmn2  30695  isdomn3  31408  bits0ALTV  32593  cdlemefrs29pre00  36537  cdlemefrs29cpre1  36540
  Copyright terms: Public domain W3C validator