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

Theorem baibr 873
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 872 . 2  |-  ( ps 
->  ( ph  <->  ch )
)
32bicomd 193 1  |-  ( ps 
->  ( ch  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  rbaibr  875  pm5.44  878  exmoeu2  2324  ssnelpss  3691  brinxp  4940  copsex2ga  6408  canth  6539  riotaxfrd  6581  iscard  7862  kmlem14  8043  ltxrlt  9146  elioo5  10968  prmind2  13090  pcelnn  13243  isnirred  15805  isreg2  17441  kqcldsat  17765  elmptrab  17859  itg2uba  19635  prmorcht  20961  adjeq  23438  lnopcnbd  23539  cvexchlem  23871  ismblfin  26247  ftc1anclem5  26284  topfne  26370  comppfsc  26387  isdmn2  26665  isdomn3  27500  cdlemefrs29pre00  31192  cdlemefrs29cpre1  31195
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator