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  2293  ssnelpss  3849  brinxp  5008  copsex2ga  5058  canth  6157  riotaxfrd  6191  iscard  8255  kmlem14  8442  ltxrlt  9555  elioo5  11463  prmind2  13891  pcelnn  14053  isnirred  16914  isreg2  19112  kqcldsat  19437  elmptrab  19531  itg2uba  21353  prmorcht  22648  adjeq  25490  lnopcnbd  25591  cvexchlem  25923  maprnin  26181  ismblfin  28579  ftc1anclem5  28618  topfne  28709  comppfsc  28726  isdmn2  29002  isdomn3  29719  cdlemefrs29pre00  34362  cdlemefrs29cpre1  34365
  Copyright terms: Public domain W3C validator