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

Theorem baibr 912
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 911 . 2  |-  ( ps 
->  ( ph  <->  ch )
)
32bicomd 204 1  |-  ( ps 
->  ( ch  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  rbaibrOLD  916  pm5.44  919  exmoeu2  2293  ssnelpss  3857  brinxp  4912  copsex2ga  4961  canth  6260  riotaxfrd  6293  iscard  8410  kmlem14  8593  ltxrlt  9704  elioo5  11692  prmind2  14620  pcelnn  14804  isnirred  17913  isreg2  20377  comppfsc  20531  kqcldsat  20732  elmptrab  20826  itg2uba  22685  prmorcht  24089  adjeq  27571  lnopcnbd  27672  cvexchlem  28004  maprnin  28307  topfne  31000  ismblfin  31892  ftc1anclem5  31932  isdmn2  32199  cdlemefrs29pre00  33878  cdlemefrs29cpre1  33881  isdomn3  35998  bits0ALTV  38517
  Copyright terms: Public domain W3C validator