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

Theorem baibr 897
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 896 . 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:  rbaibr  899  pm5.44  902  exmoeu2  2282  ssnelpss  3737  brinxp  4896  copsex2ga  4946  canth  6044  riotaxfrd  6078  iscard  8137  kmlem14  8324  ltxrlt  9437  elioo5  11345  prmind2  13766  pcelnn  13928  isnirred  16780  isreg2  18956  kqcldsat  19281  elmptrab  19375  itg2uba  21196  prmorcht  22491  adjeq  25290  lnopcnbd  25391  cvexchlem  25723  maprnin  25982  ismblfin  28385  ftc1anclem5  28424  topfne  28515  comppfsc  28532  isdmn2  28808  isdomn3  29525  cdlemefrs29pre00  33879  cdlemefrs29cpre1  33882
  Copyright terms: Public domain W3C validator