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

Theorem baibr 904
Description: Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
Hypothesis
Ref Expression
baib.1
Assertion
Ref Expression
baibr

Proof of Theorem baibr
StepHypRef Expression
1 baib.1 . . 3
21baib 903 . 2
32bicomd 201 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  rbaibrOLD  908  pm5.44  911  exmoeu2  2311  ssnelpss  3890  brinxp  5067  copsex2ga  5119  canth  6254  riotaxfrd  6288  iscard  8377  kmlem14  8564  ltxrlt  9676  elioo5  11611  prmind2  14228  pcelnn  14393  isnirred  17349  isreg2  19878  comppfsc  20033  kqcldsat  20234  elmptrab  20328  itg2uba  22150  prmorcht  23452  adjeq  26854  lnopcnbd  26955  cvexchlem  27287  maprnin  27554  ismblfin  30055  ftc1anclem5  30094  topfne  30172  isdmn2  30452  isdomn3  31164  cdlemefrs29pre00  36121  cdlemefrs29cpre1  36124
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
  Copyright terms: Public domain W3C validator