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

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

Proof of Theorem biimpar
StepHypRef Expression
1 biimpa.1 . . 3
21biimprd 223 . 2
32imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  exbiri  622  bitr  708  oplem1  964  eqtr  2483  opabss  4513  euotd  4753  xpsspw  5121  brcogw  5176  somin1  5408  xpdifid  5440  funfni  5686  fnco  5694  fnssres  5699  fn0  5705  fnimadisj  5706  fnimaeq0  5707  foco  5810  foimacnv  5838  fvelimab  5929  dffv2  5946  fvopab3ig  5953  dff3  6044  dffo4  6047  f1eqcocnv  6204  isomin  6233  f1ocnv2d  6526  fnexALT  6766  xp1st  6830  xp2nd  6831  iinon  7030  tfr3  7087  oawordri  7218  oaass  7229  omeulem1  7250  oeoa  7265  oeoe  7267  oeeulem  7269  ecelqsg  7385  elqsn0  7399  pwdom  7689  marypha1lem  7913  wofib  7991  cantnff  8114  cantnfp1  8121  cantnf  8133  cantnfp1OLD  8147  cantnfOLD  8155  cnfcomlem  8164  cnfcomlemOLD  8172  r1sscl  8224  rankval3b  8265  infxpidm2  8415  numdom  8440  onssnum  8442  acni  8447  acni2  8448  dfac5  8530  cdalepw  8597  infunsdom1  8614  infunsdom  8615  cofsmo  8670  cfsmolem  8671  fin1ai  8694  fin2i  8696  isf34lem1  8773  fin67  8796  itunisuc  8820  axdc3lem4  8854  zornn0g  8906  ttukeylem6  8915  brdom3  8927  tsken  9153  tskcard  9180  r1tskina  9181  intgru  9213  prlem934  9432  ltexprlem7  9441  uzindOLD  10982  xrmaxeq  11409  xrmineq  11410  xmulneg1  11490  ixxun  11574  difelfzle  11817  ssfzoulel  11906  elfznelfzo  11915  btwnzge0  11961  ltdifltdiv  11966  ioopnfsup  11991  icopnfsup  11992  modifeq2int  12049  suppssfz  12100  faclbnd4lem4  12374  hasheni  12421  hashgt0  12456  hashge1  12457  hashprb  12462  lennncl  12563  ccatsymb  12600  ccatlid  12603  ccatass  12605  swrdid  12652  swrdlend  12656  swrdnd  12657  swrdvalodm2  12664  ccatswrd  12681  swrdccat2  12683  swrdccat  12718  revccat  12740  cnpart  13073  resqreu  13086  recval  13155  abs1m  13168  abslem2  13172  fzomaxdiflem  13175  sqreulem  13192  sqreu  13193  limsupgre  13304  rlimdiv  13468  fsumparts  13620  climcnds  13663  expcnv  13675  ntrivcvg  13706  ndvdssub  14065  sadcaddlem  14107  rplpwr  14194  dvdssqlem  14197  algcvgblem  14206  eucalgcvga  14215  powm2modprm  14328  coprimeprodsq  14333  pythagtriplem11  14349  pythagtriplem13  14351  pcadd2  14409  4sqlem11  14473  vdwlem6  14504  vdwlem8  14506  vdwlem10  14508  ramval  14526  ramcl2  14534  ramlb  14537  ram0  14540  mreintcl  14992  mrcval  15007  mrccl  15008  mrcuni  15018  mrcun  15019  acsfiel  15051  rescabs  15202  funcres  15265  setcmon  15414  setcepi  15415  yonffthlem  15551  pleval2i  15594  pospo  15603  poslubdg  15779  acsdrsel  15797  acsdrscl  15800  acsficl  15801  psss  15844  grpidd  15895  ismndd  15943  gsumccat  16009  gsumwmhm  16013  subgmulg  16215  resghm  16283  conjnsg  16302  f1otrspeq  16472  pmtrval  16476  pmtrrn  16482  pmtrfinv  16486  pmtrprfval  16512  psgnunilem1  16518  psgnunilem5  16519  psgnunilem4  16522  psgneldm2i  16530  lsmelvalix  16661  pj1ghm  16721  efgredlemc  16763  frgp0  16778  qusabl  16871  cycsubgcyg  16903  gsumval3OLD  16908  gsumval3  16911  gsumcllem  16912  gsumcllemOLD  16913  ablfac1c  17122  pgpfac1lem5  17130  isringd  17233  lspsneq0b  17659  lmodindp1  17660  lmhmf1o  17692  lmhmpreima  17694  reslmhm  17698  pwssplit3  17707  lspsncmp  17762  lspsneq  17768  mpfind  18205  znf1o  18590  dsmmlss  18775  frlmlbs  18831  frlmup1  18832  mat1  18949  chfacfisf  19355  chfacfisfcpmat  19356  uniopn  19406  ntrval  19537  clsval  19538  neival  19603  neiptopreu  19634  lpval  19640  restdis  19679  lmbrf  19761  cnpnei  19765  1stcrest  19954  hauspwdom  20002  lfinpfin  20025  txcnpi  20109  ptrescn  20140  xkococnlem  20160  qtopeu  20217  kqreglem1  20242  ptuncnv  20308  filss  20354  fsubbas  20368  fbasrn  20385  cfinfil  20394  ufinffr  20430  elfm3  20451  rnelfmlem  20453  rnelfm  20454  flimclslem  20485  flfval  20491  isfcf  20535  cnextfvval  20565  cnextf  20566  cnextcn  20567  ustelimasn  20725  trust  20732  restutop  20740  ustuqtop2  20745  utop2nei  20753  ucncn  20788  trcfilu  20797  cnextucn  20806  met1stc  21024  metustexhalfOLD  21066  metustexhalf  21067  cfilucfilOLD  21072  cfilucfil  21073  metutopOLD  21085  psmetutop  21086  nmoix  21236  nmoeq0  21243  idnghm  21250  blcvx  21303  xrsxmet  21314  iccntr  21326  icccmp  21330  iihalf1  21431  iihalf2  21433  xrhmeo  21446  cnheibor  21455  ipcau2  21677  lmmbrf  21701  iscauf  21719  cmetcaulem  21727  bcthlem4  21766  cmetcuspOLD  21793  cmetcusp  21794  rrxcph  21824  minveclem4  21847  evthicc2  21872  cniccbdd  21873  ovollb2  21900  ovolunlem1a  21907  ovolunlem1  21908  voliun  21964  icombl  21974  ioombl  21975  iccvolcl  21977  ioovolcl  21979  mbfss  22053  mbfposb  22060  itg2const2  22148  itg2splitlem  22155  itg2gt0  22167  iblss2  22212  itgioo  22222  dvaddf  22345  dvmulf  22346  dvcobr  22349  dvcof  22351  rolle  22391  dvlip  22394  c1lip1  22398  dvivthlem1  22409  lhop1lem  22414  dvfsumlem1  22427  ftc1lem4  22440  ftc1lem5  22441  ply1divmo  22536  coe1termlem  22655  plydiveu  22694  taylplem1  22758  pserulm  22817  abelth  22836  abscxp2  23074  abscxpbnd  23127  ang180lem2  23142  ang180lem3  23143  isosctrlem1  23152  angpieqvd  23162  atandmtan  23251  birthdaylem3  23283  wilthlem2  23343  isppw  23388  isppw2  23389  dvdsflsumcom  23464  chteq0  23484  perfectlem2  23505  dchrval  23509  dchrinvcl  23528  dchrptlem1  23539  bposlem3  23561  lgsmod  23596  lgsdilem  23597  lgsdir2lem2  23599  lgsdir2  23603  lgsne0  23608  lgseisenlem1  23624  2sqlem4  23642  chpo1ubb  23666  dchrisumn0  23706  pntrsumbnd2  23752  ostthlem1  23812  ostth3  23823  idmot  23924  tgelrnln  24010  lmimid  24159  lmiisolem  24161  hypcgrlem1  24164  brcgr  24203  colinearalglem4  24212  colinearalg  24213  axlowdimlem14  24258  axcontlem4  24270  uvtxnbgravtx  24495  wlknwwlknsur  24712  clwlkisclwwlklem2fv2  24783  frghash2spot  25063  gxcom  25271  resgrprn  25282  ghabloOLD  25371  nvss  25486  sspn  25649  nmoub3i  25688  nmblolbii  25714  blocnilem  25719  minvecolem4  25796  htthlem  25834  norm1  26167  norm1exi  26168  pjeq  26317  axpjpj  26338  normcan  26494  pjoi0  26635  nmopub2tALT  26828  nmfnleub2  26845  eighmorth  26883  nmbdoplbi  26943  nmcoplbi  26947  nmophmi  26950  nmbdfnlbi  26968  nmcfnlbi  26971  riesz3i  26981  cnlnadjlem7  26992  branmfn  27024  nmopleid  27058  hstle  27149  superpos  27273  cvexchlem  27287  foresf1o  27403  elabreximd  27408  f1o3d  27471  funcnvmptOLD  27509  funcnvmpt  27510  fgreu  27513  resf1o  27553  fpwrelmap  27556  mul2lt0rlt0  27565  xrofsup  27582  eliccelico  27588  elicoelioo  27589  iocinif  27592  difioo  27593  eliccioo  27627  submomnd  27700  archirngz  27733  gsummpt2co  27771  ornglmullt  27797  orngrmullt  27798  qtophaus  27839  locfinreflem  27843  crefi  27850  unitdivcld  27883  tpr2rico  27894  ordtrestNEW  27903  lmxrge0  27934  elzrhunit  27960  qqhf  27967  indf1ofs  28039  gsumesum  28067  esumfsup  28076  esumcvg  28092  issgon  28123  sigainb  28136  insiga  28137  isrnmeas  28171  measvunilem  28183  volmeas  28203  ddeval1  28206  ddeval0  28207  imambfm  28233  eulerpartlemf  28309  eulerpartlemgvv  28315  probun  28358  dstfrvunirn  28413  plymulx  28505  signslema  28519  signstfvn  28526  signsvtn0  28527  signstfvneq0  28529  signstres  28532  signstfveq0a  28533  derangen  28616  subfacp1lem2b  28625  subfacp1lem4  28627  subfacp1lem5  28628  derangfmla  28634  ptpcon  28678  mppspstlem  28931  wfr3g  29342  wfrlem3  29345  wfrlem4  29346  wsuclem  29381  frr3g  29386  frrlem3  29389  nocvxmin  29451  nobndlem6  29457  nobndup  29460  nobnddown  29461  colinearex  29710  btwnconn1lem11  29747  btwnconn1lem12  29748  fin2so  30040  supaddc  30041  heicant  30049  mblfinlem2  30052  voliunnfl  30058  mbfresfi  30061  itg2addnclem  30066  itg2addnclem3  30068  itg2gt0cn  30070  ftc1cnnclem  30088  ftc1anclem5  30094  gtinf  30137  nn0prpwlem  30140  cover2  30204  indexdom  30225  sdclem1  30236  fdc  30238  equivbnd2  30288  heiborlem8  30314  heibor  30317  isdrngo2  30361  iscringd  30396  smprngopr  30449  prnc  30464  nacsfix  30644  3rexfrabdioph  30730  4rexfrabdioph  30731  6rexfrabdioph  30732  7rexfrabdioph  30733  eldioph4b  30745  pellexlem2  30766  pellexlem5  30769  expmordi  30883  jm2.26lem3  30943  numinfctb  31052  cvgdvgrat  31194  radcnvrat  31195  dvconstbi  31239  bccbc  31250  cncfiooicclem1  31696  ibliooicc  31770  stoweidlem27  31809  stoweidlem28  31810  fourierdlem89  31978  fourierdlem91  31980  fourierdlem92  31981  fullestrcsetc  32657  funcsetcestrclem8  32668  fullsetcestrc  32672  onetansqsecsq  33155  cotsqcscsq  33156  aacllem  33216  elpwgded  33337  elpwgdedVD  33717  sspwimpcf  33720  sspwimpcfVD  33721  sspwimpALT2  33728  ax6e2ndeqALT  33731  bnj529  33798  bnj548  33955  bnj570  33963  bnj852  33979  bnj929  33994  bnj1097  34037  bnj1118  34040  bnj1145  34049  bj-flbi3  34608  islfld  34787  lkrshpor  34832  lfl1dim  34846  lfl1dim2N  34847  cmtcomlemN  34973  2lplnmN  35283  pmapjat1  35577  trlnid  35904  tendoex  36701  dia1dimid  36790  dibval2  36871  dihmeetlem2N  37026  dochlkr  37112  mapdcv  37387  hdmaplkr  37643  hdmapip0  37645  hlhillcs  37688
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