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

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

Proof of Theorem biimpa
StepHypRef Expression
1 biimpa.1 . . 3
21biimpd 207 . 2
32imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  simprbda  623  simplbda  624  pm5.1  857  bimsc1  938  biimp3a  1328  equsex  2038  euor  2331  euan  2351  cgsexg  3142  cgsex2g  3143  cgsex4g  3144  ceqsex  3145  sbciegft  3358  sbeqalb  3384  syl5sseq  3551  elpwunsn  4070  ralxfr2d  4668  euotd  4753  relop  5158  fnbr  5688  f1o00  5853  foelrni  5921  dffv2  5946  iinpreima  6017  funressn  6084  fnex  6139  weniso  6250  f1ocnv2d  6526  ofrval  6550  limsssuc  6685  resiexg  6736  eloprabi  6862  1stconst  6888  2ndconst  6889  frxp  6910  poxp  6912  smodm2  7045  smoiso  7052  tz7.44lem1  7090  oev2  7192  oesuclem  7194  oecl  7206  omordi  7234  omwordri  7240  omword2  7242  omordlim  7245  omlimcl  7246  omeulem2  7251  oeordi  7255  oewordri  7260  oelim2  7263  oeoa  7265  oeoe  7267  nnawordi  7289  nnaordex  7306  erth  7375  iiner  7402  pw2f1olem  7641  pw2f1o  7642  onomeneq  7727  onfin2  7729  unxpdomlem2  7745  isinf  7753  findcard2  7780  fipreima  7846  fipwss  7909  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  carden2b  8369  carddomi2  8372  infxpenlem  8412  acni2  8448  numacn  8451  alephfp  8510  pwsdompw  8605  ackbij2lem3  8642  cfeq0  8657  cfsuc  8658  cfsmolem  8671  domfin4  8712  axdc3lem2  8852  axdc3lem4  8854  alephreg  8978  fpwwe2  9042  winainflem  9092  r1limwun  9135  inar1  9174  grudomon  9216  nlt1pi  9305  indpi  9306  nqereu  9328  ltbtwnnq  9377  prlem934  9432  prlem936  9446  addgt0sr  9502  leltne  9695  ne0gt0  9710  mullt0  10097  msqgt0  10098  mulne0  10216  divne0  10244  div2neg  10292  ltmul12a  10423  recgt1i  10467  nn2ge  10586  nn0lt2  10952  peano5uzi  10976  eluzp1m1  11133  eluzaddi  11136  eluzsubi  11137  uz2m1nn  11185  nn01to3  11204  rpnnen1lem5  11241  rphalflt  11275  xrleltne  11380  max0sub  11424  xmulpnf1n  11499  xmulge0  11505  xadddi  11516  supxr  11533  supxr2  11534  ixxdisj  11573  ixxun  11574  ixxub  11579  ixxlb  11580  iccgelb  11610  icodisj  11674  difreicc  11681  iccf1o  11693  fzsuc2  11766  fzonmapblen  11868  elfznelfzo  11915  flge0nn0  11954  flge1nn  11955  2submod  12048  seqf1olem2  12147  expubnd  12226  sqlecan  12274  bernneq  12292  bernneq2  12293  expnbnd  12295  discr1  12302  facwordi  12367  faclbnd4lem4  12374  bcpasc  12399  hashgt0n0  12435  elprchashprn2  12461  hash1to3  12530  iswrdi  12552  ffz0iswrd  12568  wrdsymb0  12575  ccatsymb  12600  ccatass  12605  swrdspsleq  12673  swrdswrdlem  12684  swrdswrd  12685  swrdswrd0  12687  swrdccatin12lem2b  12711  revccat  12740  revrev  12741  repswccat  12757  2cshw  12781  cshwcsh2id  12796  revco  12800  cshco  12802  s2f1o  12864  s4f1o  12866  wrdlen2i  12884  wwlktovf  12894  sqr0lem  13074  sqrlem2  13077  sqrlem7  13082  max0add  13143  recval  13155  nnabscl  13158  absmax  13162  sqreulem  13192  climi0  13335  lo1bdd2  13347  rlimresb  13388  lo1eq  13391  rlimeq  13392  isercolllem3  13489  climsup  13492  fsumsplit  13562  fsumcom2  13589  explecnv  13676  fprodser  13756  fprodsplit  13770  fprodcom2  13788  eftlub  13844  sin02gt0  13927  rpnnen2lem10  13957  mulmoddvds  14044  odd2np1  14046  oexpneg  14049  bitsf1  14096  sadcaddlem  14107  bitsuz  14124  rplpwr  14194  rppwr  14195  nn0seqcvgd  14199  qredeq  14247  qgt0numnn  14284  phibndlem  14300  reumodprminv  14329  coprimeprodsq2  14334  pythagtrip  14358  fldivp1  14416  unbenlem  14426  4sqlem9  14464  4sqlem15  14477  4sqlem16  14478  vdwlem6  14504  vdwlem10  14508  vdwlem11  14509  vdwlem13  14511  vdw  14512  cshwshashlem1  14580  mreuni  14997  cidpropd  15105  subsubc  15222  ffthiso  15298  fuciso  15344  setcmon  15414  setcepi  15415  catciso  15434  hofcl  15528  hofpropd  15536  yonedalem4c  15546  yonedainv  15550  imasmnd  15958  pwsco1mhm  16001  imasgrp  16186  subginv  16208  subgmulg  16215  eqger  16251  subgga  16338  orbstafun  16349  orbsta  16351  symggrp  16425  psgnsn  16545  dfod2  16586  gexval  16598  gex1  16611  sylow2blem1  16640  sylow3lem1  16647  pj1eu  16714  efgredlema  16758  frgp0  16778  frgpmhm  16783  odadd1  16854  0cyg  16895  gsumzres  16914  gsumzresOLD  16918  gsumzsplit  16944  gsumzsplitOLD  16945  gsummptfzcl  16996  dprd2dlem1  17090  dprd2da  17091  dmdprdsplit2  17095  dprdsplit  17097  pgpfaclem3  17134  ablfac2  17140  imasring  17268  rhmf1o  17381  kerf1hrm  17392  subrg1  17439  abvneg  17483  lmhmf1o  17692  lmhmima  17693  reslmhm2b  17700  pwssplit0  17704  pwssplit1  17705  lsmspsn  17730  lspdisj  17771  lidlmcl  17865  isnzr2hash  17912  fidomndrnglem  17955  mplsubglem  18093  mplsubglemOLD  18095  mplmonmul  18126  mplbas2  18134  mplbas2OLD  18135  subrgascl  18163  subrgasclcl  18164  evlsval2  18189  mpfind  18205  lply1binomsc  18349  absabv  18475  frlmbasOLD  18787  f1lindf  18857  mat0dimscm  18971  scmataddcl  19018  scmatsubcl  19019  smatvscl  19026  mdetunilem8  19121  chfacfscmul0  19359  chfacfscmulfsupp  19360  chfacfscmulgsum  19361  chfacfpmmul0  19363  chfacfpmmulfsupp  19364  chfacfpmmulgsum  19365  cpmidpmatlem3  19373  chcoeffeqlem  19386  cayleyhamilton0  19390  cayleyhamiltonALT  19392  cayleyhamilton1  19393  elcls  19574  clsndisj  19576  isclo2  19589  neiuni  19623  neissex  19628  neiptopreu  19634  tgrest  19660  neitr  19681  tgcnp  19754  lmfpm  19796  lmcl  19798  lmss  19799  lmff  19802  ist1-2  19848  cnt1  19851  cmpsublem  19899  clscon  19931  locfindis  20031  kgeni  20038  kgenidm  20048  txcnpi  20109  ptpjopn  20113  ptclsg  20116  txcmplem1  20142  qtoptop2  20200  qtoptopon  20205  r0sep  20249  ptunhmeo  20309  t0kq  20319  fsubbas  20368  neifil  20381  uffixsn  20426  ufildr  20432  rnelfm  20454  isfcls2  20514  uffclsflim  20532  alexsublem  20544  cnextfun  20564  cnextfvval  20565  cnextf  20566  cnextcn  20567  tmdcn2  20588  symgtgp  20600  tsmssplit  20654  ustuni  20729  trust  20732  utoptop  20737  restutop  20740  restutopopn  20741  ustuqtop1  20744  ustuqtop2  20745  ustuqtop3  20746  ustuqtop4  20747  utop2nei  20753  utop3cls  20754  ucncn  20788  trcfilu  20797  cfiluweak  20798  psmetdmdm  20809  xmeter  20936  prdsbl  20994  neibl  21004  methaus  21023  prdsxmslem2  21032  metusttoOLD  21060  metustto  21061  metustexhalfOLD  21066  metustexhalf  21067  metustOLD  21070  metust  21071  cfilucfilOLD  21072  cfilucfil  21073  metutopOLD  21085  psmetutop  21086  metucnOLD  21091  tngngp2  21166  tngngp  21168  tgqioo  21305  xrsxmet  21314  icccmplem1  21327  icccmplem2  21328  cnmpt2pc  21428  iihalf2  21433  icoopnst  21439  iocopnst  21440  xrhmeo  21446  lebnumlem1  21461  lebnumlem3  21463  pi1blem  21539  pi1grplem  21549  pi1xfrf  21553  pi1xfr  21555  pi1xfrcnvlem  21556  pi1cof  21559  pi1coghm  21561  cmetcaulem  21727  causs  21737  metcld  21744  lmcau  21751  rrxcph  21824  minveclem4  21847  ivthlem2  21864  ivthlem3  21865  ivthicc  21870  ovolshftlem1  21920  ovolicc1  21927  ovolicopnf  21935  volfiniun  21957  uniioombllem3  21994  dyaddisjlem  22004  vitalilem2  22018  itg1ge0  22093  mbfi1fseqlem3  22124  xrge0f  22138  itg2seq  22149  itg2monolem1  22157  itg2addlem  22165  itg2gt0  22167  iblcnlem  22195  itgss3  22221  itgsplit  22242  dvnff  22326  dvferm2  22388  dvlip2  22396  dveq0  22401  dvge0  22407  dvcnvre  22420  dvfsumle  22422  dvfsumabs  22424  dvfsumlem2  22428  ftc1lem2  22437  ftc1lem4  22440  ftc1lem5  22441  ftc1cn  22444  ftc2  22445  itgsubstlem  22449  coe1mul3  22500  ply1divex  22537  dgrlem  22626  dgrlb  22633  coemulhi  22651  dgrlt  22663  dgrmul  22667  plydivlem4  22692  fta1  22704  aaliou2b  22737  taylplem2  22759  dvtaylp  22765  ulmcau  22790  tanabsge  22899  sinq12gt0  22900  argimgt0  22997  cxplea  23077  cxple2  23078  cxpsqrt  23084  cxpaddlelem  23125  loglesqrt  23132  ang180lem2  23142  lawcos  23148  logrec  23151  asinlem3a  23201  asinlem3  23202  asinsin  23223  atanlogaddlem  23244  atanlogadd  23245  atanlogsub  23247  atantan  23254  atanbnd  23257  atantayl2  23269  efrlim  23299  wilthlem2  23343  basellem2  23355  sqfpc  23411  ppieq0  23450  sqff1o  23456  fsumdvdscom  23461  ppiub  23479  chpeq0  23483  chtleppi  23485  fsumvma  23488  fsumvma2  23489  mersenne  23502  dchrabs2  23537  dchr1re  23538  dchrpt  23542  lgsdilem  23597  lgsdinn0  23615  lgsquad3  23636  m1lgs  23637  2sqlem6  23644  rpvmasumlem  23672  dchrisumlem3  23676  dchrisum0flblem1  23693  pntibndlem2a  23775  pntlem3  23794  padicabv  23815  ercgrg  23908  tglnunirn  23935  tglineeltr  24011  mirln2  24057  mirbtwnhl  24060  isperp2  24092  lnopp2hpgb  24132  ttgbtwnid  24187  axcontlem2  24268  axcontlem12  24278  usgra1  24373  edgprvtx  24385  usgraedg4  24387  nbgraop  24423  nbgracnvfv  24440  nbcusgra  24463  wlkdvspthlem  24609  fargshiftf1  24637  fargshiftfo  24638  wlkiswwlk1  24690  clwlkisclwwlklem2a4  24784  clwlkisclwwlk2  24790  clwwlkf1  24796  clwwnisshclwwn  24809  eleclclwwlknlem2  24818  erclwwlkneqlen  24824  clwlkfclwwlk2wrd  24840  clwlkf1clwwlklem3  24848  clwlkf1clwwlklem  24849  usg2spthonot  24888  eupatrl  24968  eupap1  24976  frgrancvvdeqlemA  25037  frgrancvvdeqlemB  25038  frgrancvvdeqlemC  25039  frgrawopreglem4  25047  numclwwlkovf2ex  25086  numclwwlk2lem1  25102  frgrareggt1  25116  frgraregord013  25118  vcoprnelem  25471  cnnv  25582  nmounbseqi  25692  nmounbseqiOLD  25693  nmlnogt0  25712  nmblolbii  25714  blocnilem  25719  ajmoi  25774  minvecolem4  25796  hhnv  26082  norm1  26167  hhssnv  26180  pjhtheu  26312  pjpreeq  26316  spanunsni  26497  fh1  26536  fh2  26537  cm2j  26538  chscllem4  26558  pjid  26613  adjmo  26751  eleigveccl  26878  eigvalcl  26880  eigvec1  26881  eighmre  26882  eighmorth  26883  nmop0h  26910  nmbdoplbi  26943  nmcoplbi  26947  nmophmi  26950  lncnopbd  26956  nmbdfnlbi  26968  nmcfnlbi  26971  cnlnadjeui  26996  branmfn  27024  rnbra  27026  nmopleid  27058  strlem5  27174  hstrlem5  27182  dmdbr3  27224  dmdbr4  27225  mdsl3  27235  hatomistici  27281  cvexchlem  27287  chirredlem1  27309  chirredlem2  27310  chirredi  27313  atcvat3i  27315  atcvat4i  27316  atabsi  27320  mdsymlem1  27322  mdsymlem3  27324  mdsymlem5  27326  dmdbr5ati  27341  cdj1i  27352  foresf1o  27403  rabfodom  27404  elabreximd  27408  elpreq  27417  f1o3d  27471  disjdsct  27521  fcobij  27548  fpwrelmapffslem  27555  nn0sqeq1  27562  xrofsup  27582  eliccelico  27588  elicoelioo  27589  numdenneg  27608  xrge0addgt0  27681  xrge0adddir  27682  xrge0npcan  27684  omndmul3  27703  submarchi  27730  archirng  27732  archirngz  27733  archiexdiv  27734  archiabllem1a  27735  locfinreflem  27843  metideq  27872  unitdivcld  27883  cnre2csqlem  27892  ordtconlem1  27906  fmcncfil  27913  lmxrge0  27934  pl1cn  27937  zrhunitpreima  27959  elzdif0  27961  qqhval2lem  27962  qqhf  27967  indf1ofs  28039  esumfsup  28076  esumpcvgval  28084  sigasspw  28116  issgon  28123  meascnbl  28190  voliune  28201  volfiniune  28202  oddpwdc  28293  eulerpartlems  28299  eulerpartlemgvv  28315  ballotlemfrcn0  28468  ballotlemirc  28470  sgncl  28477  sgnneg  28479  sgn3da  28480  sgnmul  28481  sgnsub  28483  gsumnunsn  28493  ofccat  28497  signsplypnf  28507  signsply0  28508  signslema  28519  signstfvneq0  28529  signsvfpn  28542  signsvfnn  28543  subfacp1lem5  28628  subfacp1lem6  28629  erdszelem9  28643  ptpcon  28678  rescon  28691  cvmlift3lem7  28770  msrrcl  28903  sspred  29252  trpredrec  29321  btwnintr  29669  btwnouttr  29674  cgrxfr  29705  btwnconn1lem12  29748  colinbtwnle  29768  lineelsb2  29798  onintopsscon  29905  heicant  30049  mblfinlem2  30052  itg2gt0cn  30070  itgaddnclem2  30074  ftc1cnnclem  30088  ftc1cnnc  30089  ftc1anclem2  30091  ftc1anclem5  30094  ftc1anclem7  30096  ftc1anc  30098  ftc2nc  30099  dvasin  30103  areacirclem5  30111  areacirc  30112  nn0prpwlem  30140  neibastop3  30180  fdc  30238  incsequz  30241  blbnd  30283  prdstotbnd  30290  cnpwstotbnd  30293  ismtyres  30304  rngohomf  30369  rngohom1  30371  rngohomadd  30372  rngohommul  30373  idlss  30413  idl0cl  30415  idladdcl  30416  idllmulcl  30417  idlrmulcl  30418  maxidlnr  30439  maxidlmax  30440  smprngopr  30449  pridlc  30468  ac6s6f  30581  ceqsex3OLD  30601  mzpindd  30678  lzunuz  30701  2rexfrabdioph  30729  irrapxlem3  30760  pellexlem2  30766  pellexlem5  30769  pell1234qrreccl  30790  pell14qrdich  30805  pell1qrge1  30806  elpell1qr2  30808  reglogltb  30827  reglogleb  30828  rmxycomplete  30853  2nn0ind  30881  congabseq  30912  acongrep  30918  acongeq  30921  dvdsleabs2  30926  jm2.22  30937  jm2.26lem3  30943  pw2f1ocnv  30979  limsuc2  30986  fnwe2lem3  30998  aomclem6  31005  kercvrlsm  31029  pwssplit4  31035  lpirlnr  31066  hashgcdeq  31158  isprm7  31192  cvgdvgrat  31194  radcnvrat  31195  lcmneg  31209  dvconstbi  31239  bccbc  31250  mulltgt0  31397  refsumcn  31405  cncmpmax  31407  icoiccdif  31564  climinf  31612  climreeq  31619  coskpi2  31666  cosknegpi  31669  icccncfext  31690  dvmptfprodlem  31741  stoweidlem27  31809  stoweidlem29  31811  stoweidlem31  31813  stoweidlem34  31816  stoweidlem48  31830  stoweidlem59  31841  fourierdlem109  31998  fourierswlem  32013  etransclem37  32054  sigarcol  32081  reuan  32185  ndmaovg  32269  subsubelfzo0  32338  usgra2pthlem1  32353  usgvincvad  32404  usgvincvadALT  32407  funcestrcsetclem7  32652  funcestrcsetclem8  32653  setc1strwun  32659  funcsetcestrclem7  32667  rnghmf1o  32709  rnghmsubcsetclem1  32783  zrinitorngc  32808  zrtermorngc  32809  rhmsubcsetclem1  32829  rhmsubcrngclem1  32835  funcringcsetcOLD2lem8  32851  funcringcsetclem8OLD  32874  zrtermoringc  32878  ply1sclrmsm  32983  lincfsuppcl  33014  bi2imp  33251  ax6e2ndeqALT  33731  bnj563  33800  bnj1001  34016  bj-equsexv  34312  bj-equsexvv  34313  lshpnel2N  34710  islsati  34719  lkr0f  34819  lfl1dim  34846  lfl1dim2N  34847  omlfh1N  34983  leat  35018  atlatmstc  35044  cvlatexch3  35063  lnnat  35151  cvrat3  35166  cvrat4  35167  3dim3  35193  dalem4  35389  dalem39  35435  paddasslem12  35555  psubcliN  35662  pmapojoinN  35692  lhpm0atN  35753  lhprelat3N  35764  trlnid  35904  trlval3  35912  cdleme22b  36067  trljco  36466  diaglbN  36782  dibvalrel  36890  dicvalrelN  36912  diclspsn  36921  dih1dimatlem  37056  dihlatat  37064  lcfl6  37227  lcfl8  37229  lcfrvalsnN  37268  lcfrlem9  37277  mapdheq2  37456  hlhillcs  37688  hlhilhillem  37690  taupilem1  37696
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