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

Theorem biimparc 487
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1
Assertion
Ref Expression
biimparc

Proof of Theorem biimparc
StepHypRef Expression
1 biimpa.1 . . 3
21biimprcd 225 . 2
32imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  biantr  931  elrab3t  3256  difprsnss  4165  elpw2g  4615  elon2  4894  ideqg  5159  elrnmpt1s  5255  elrnmptg  5257  eqfnfv2  5982  fmpt  6052  elunirn  6163  fun11iun  6760  tposfo2  6997  tposf12  6999  dom2lem  7575  enfii  7757  ssnnfi  7759  ac6sfi  7784  unfilem1  7804  inf3lem2  8067  infdiffi  8095  dfac5lem5  8529  dfac2  8532  dfac12k  8548  cfslb2n  8669  enfin2i  8722  fin23lem19  8737  axdc2lem  8849  axdc3lem4  8854  winainflem  9092  indpi  9306  ltexnq  9374  ltbtwnnq  9377  ltexprlem6  9440  prlem936  9446  elreal2  9530  fimaxre3  10517  expnbnd  12295  repswswrd  12756  climcnds  13663  fprod2dlem  13784  unbenlem  14426  acsfn  15056  lsmcv  17787  maducoeval2  19142  bastop2  19496  neipeltop  19630  rnelfmlem  20453  isfcls  20510  tgphaus  20615  mbfi1fseqlem4  22125  ulm2  22780  ax5seglem5  24236  wlkdvspthlem  24609  wlknwwlknsur  24712  spanunsni  26497  nonbooli  26569  nmopun  26933  lncnopbd  26956  pjnmopi  27067  sumdmdlem  27337  spc2ed  27372  rnmpt2ss  27515  esumpcvgval  28084  soseq  29334  btwnconn1lem7  29743  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  ivthALT  30153  topfneec  30173  fdc  30238  ismtyres  30304  isdrngo3  30362  isnumbasgrplem3  31054  pm13.13b  31315  fprodle  31604  ax6e2ndeqALT  33731  sineq0ALT  33737  bnj545  33953  bnj900  33987  bnj1498  34117  bj-snglss  34528  lshpset2N  34844  3dimlem1  35182  3dim3  35193  cdleme31fv2  36119
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