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

Theorem biimpd 207
Description: Deduce an implication from a logical equivalence. (Contributed by NM, 11-Jan-1993.)
Hypothesis
Ref Expression
biimpd.1
Assertion
Ref Expression
biimpd

Proof of Theorem biimpd
StepHypRef Expression
1 biimpd.1 . 2
2 bi1 186 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  mpbid  210  sylibd  214  sylbid  215  mpbidi  216  syl5ib  219  syl6bi  228  ibi  241  con4bid  293  mtbird  301  mtbiri  303  imbi1d  317  pm5.21im  349  biimpa  484  exintr  1702  spfw  1806  cbvalw  1808  alcomiw  1811  19.9d  1892  19.23t  1909  spimt  2005  spv  2011  chvar  2013  cbval  2021  nfsb4t  2130  dral1-o  2233  2eu3  2379  eqrdav  2455  eqrdavOLD  2456  cleqhOLD  2573  rgen2a  2884  ralcom2  3022  ceqsalgALT  3135  vtoclf  3160  vtocl2  3162  vtocl3  3163  spcdv  3192  rspcdv  3213  rexraleqim  3225  elabgt  3243  sbcn1  3375  sbcim1  3376  sbcbi1  3377  sbeqalb  3384  sbcel21v  3395  eqrd  3521  elpwunsn  4070  rabsnifsb  4098  ssunsn2  4189  euotd  4753  sotr2  4834  onmindif  4972  relop  5158  elres  5314  restidsing  5335  elimasni  5369  sotri2  5401  relcnvtr  5532  iotaval  5567  dffv2  5946  mpteqb  5970  elfvmptrab  5977  chfnrn  5998  elpreima  6007  iinpreima  6017  exfo  6049  ffnfv  6057  f1elima  6171  f1eqcocnv  6204  fliftfun  6210  soisores  6223  isotr  6232  isomin  6233  ovmpt2dv2  6436  difsnexi  6608  onint  6630  oneqmin  6640  ordunisuc2  6679  tfindsg  6695  findsg  6727  f1oweALT  6784  ressuppss  6938  funsssuppss  6945  imacosupp  6959  smoiso  7052  seqomlem2  7135  oaordi  7214  oawordri  7218  oaordex  7226  oalimcl  7228  omwordi  7239  oewordi  7259  oelim2  7263  nnmwordi  7303  xpider  7401  iiner  7402  undifixp  7525  mptelixpg  7526  dom2lem  7575  nneneq  7720  fineqvlem  7754  pssnn  7758  dif1enOLD  7772  dif1en  7773  findcard2s  7781  unfilem2  7805  xpfi  7811  domunfican  7813  fsuppimp  7855  dffi2  7903  wemaplem2  7993  suc11reg  8057  noinfep  8097  cantnflem1  8129  cantnflem1OLD  8152  r1fin  8212  tcrank  8323  cardlim  8374  pr2nelem  8403  fseqenlem1  8426  alephnbtwn  8473  alephord2i  8479  alephf1  8487  cardaleph  8491  alephiso  8500  dfac12lem2  8545  ackbij1lem16  8636  cflm  8651  cfcoflem  8673  sornom  8678  fin23lem27  8729  isf32lem7  8760  fin17  8795  fin1a2lem2  8802  fin1a2lem4  8804  fin1a2lem6  8806  fin1a2lem9  8809  axdc3lem2  8852  zorn2lem7  8903  uniimadom  8940  inar1  9174  grothomex  9228  addcanpi  9298  mulcanpi  9299  enqer  9320  genpcd  9405  genpnmax  9406  ltexprlem4  9438  reclem3pr  9448  reclem4pr  9449  suplem2pr  9452  axpre-ltadd  9565  axpre-sup  9567  ltletr  9697  00id  9776  mul0or  10214  prodgt02  10413  prodge02  10415  lemul1a  10421  mulgt1  10426  divgt0  10435  divge0  10436  ledivp1i  10496  ltdivp1i  10497  cju  10557  nnsub  10599  nominpos  10800  nn0n0n1ge2  10884  btwnnz  10964  uzindOLD  10982  suprfinzcl  11003  ublbneg  11195  zmax  11208  cnref1o  11244  ltsubrp  11280  ltaddrp  11281  xrltletr  11389  qbtwnre  11427  xltnegi  11444  iccsupr  11646  icoshft  11671  difreicc  11681  iccshftri  11684  iccshftli  11686  iccdili  11688  icccntri  11690  fzen  11732  elfzmlbmOLD  11814  fzofzim  11869  eluzgtdifelfzo  11878  injresinjlem  11925  injresinj  11926  flval2  11950  flval3  11951  modaddmodup  12050  fseqsupubi  12088  ssnn0fi  12094  mptnn0fsuppr  12105  sq01  12288  hashf1rn  12425  hashle00  12465  hashgt12el  12481  hashgt12el2  12482  hash2pr  12515  hash2prb  12517  hashtpg  12523  hash3tr  12529  swrdnd  12657  swrdsymbeq  12672  2swrd1eqwrdeq  12679  ccatopth2  12696  reuccats1lem  12705  swrdccatin2  12712  swrdccat  12718  swrdccat3a  12719  swrdccat3blem  12720  repsdf2  12750  repswsymball  12751  repswrevw  12758  cshweqrep  12789  cshw1  12790  2cshwcshw  12793  scshwfzeqfzo  12794  cshwcsh2id  12796  swrdco  12803  swrd2lsw  12890  2swrd2eqwrdeq  12891  wwlktovfo  12896  cjre  12972  o1lo1  13360  o1of2  13435  o1rlimmul  13441  zsum  13540  modfsummods  13607  zprod  13744  reeff1  13855  dvds2lem  13996  muldvds1  14008  dvdscmulr  14012  dvdsmulcr  14013  divalglem8  14058  ndvdsadd  14066  gcdmultiple  14188  prmn2uzge3  14237  isprm6  14250  isprm5  14253  prmdvdsexpr  14257  divgcdodd  14260  phiprmpw  14306  modprm0  14330  pythagtriplem4  14343  pcz  14404  1arith  14445  cshwrepswhash1  14587  divsfval  14944  catsubcat  15208  fthmon  15296  setcmon  15414  setcepi  15415  pltnle  15596  pltval3  15597  lublecllem  15618  latasym  15685  odupos  15765  mrelatglb  15814  mrelatlub  15816  cnvpsb  15843  isgrpid2  16086  ghmf1  16295  orbsta  16351  resscntz  16369  gsmsymgrfixlem1  16452  gsmsymgreqlem2  16456  mndodcongi  16567  odf1  16584  lsmss1  16684  lsmss2  16686  efgredeu  16770  cntzcmnss  16849  lt6abl  16897  ablfaclem3  17138  kerf1hrm  17392  lspsneq  17768  lspsneu  17769  lsmcv  17787  lidldvgen  17903  0ringnnzr  17917  domnmuln0  17947  opprdomn  17950  ply1scln0  18332  gsummoncoe1  18346  domnchr  18569  znf1o  18590  zntoslem  18595  znfld  18599  cygznlem2a  18606  cygznlem3  18608  islindf4  18873  uvcendim  18882  matvscl  18933  scmataddcl  19018  scmatsubcl  19019  scmatfo  19032  scmatghm  19035  maducoeval2  19142  slesolinv  19182  cramerimplem2  19186  cpmatelimp  19213  cpmatelimp2  19215  cpmatacl  19217  cpmatinvcl  19218  pm2mpf1  19300  cayhamlem1  19367  cayleyhamilton1  19393  0ntr  19572  islpi  19650  lmss  19799  cmpcld  19902  cmpfi  19908  bwthOLD  19911  1stcelcls  19962  comppfsc  20033  ptcnplem  20122  qtophmeo  20318  fbdmn0  20335  fbasrn  20385  elfm3  20451  fmfnfmlem4  20458  fclscf  20526  cnpfcf  20542  alexsubALTlem3  20549  tsmsresOLD  20645  tsmsres  20646  blval2  21078  nmoleub  21238  nmhmcn  21603  iscau4  21718  caussi  21736  cniccbdd  21873  ovoliunnul  21918  mbfinf  22072  itg2splitlem  22155  dvcn  22324  c1lip1  22398  c1lip3  22400  dvcnvrelem1  22418  ply1divex  22537  quotcan  22705  aannenlem1  22724  taylf  22756  ulmcaulem  22789  ulmcau  22790  reeff1o  22842  logccv  23044  logreclem  23150  isosctrlem2  23153  xrlimcnp  23298  rlimcxp  23303  ftalem7  23352  vmappw  23390  fsumvma  23488  dchreq  23533  dchrptlem1  23539  dchrsum  23544  bposlem7  23565  lgsqrlem2  23617  lgsdchr  23623  lgseisenlem2  23625  lgsquad2  23635  2sqlem6  23644  isperp2  24092  xmstrkgc  24189  brbtwn  24202  brcgr  24203  axcgrid  24219  axeuclidlem  24265  axeuclid  24266  uhgraeq12d  24307  usgrac  24351  usgraeq12d  24362  usgranloopv  24378  nbgraf1olem5  24445  iscusgra0  24457  cusgrasize2inds  24477  cusgrafilem3  24481  usgramaxsize  24487  iswlkg  24524  wlkcompim  24526  wlkcpr  24529  wlkonprop  24535  trlonprop  24544  0wlkon  24549  usgrnloop  24565  pthonprop  24579  spthonprp  24587  redwlk  24608  wlkdvspthlem  24609  usgra2wlkspthlem2  24620  fargshiftfv  24635  wwlknimp  24687  vfwlkniswwlkn  24706  usg2wlkeq  24708  wwlknred  24723  wwlknext  24724  wwlknextbi  24725  wwlkextwrd  24728  wwlkextinj  24730  wwlkextsur  24731  wwlkm1edg  24735  isclwlkg  24755  clwlkcompim  24764  0clwlk  24765  clwwlkn2  24775  clwlkisclwwlklem2a1  24779  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwwlkf  24794  wwlkext2clwwlk  24803  clwwisshclwwlem1  24805  wlklenvclwlk  24839  clwlkfclwwlk  24844  el2spthonot  24870  usg2wotspth  24884  usg2spthonot  24888  usg2spthonot0  24889  rgraprop  24928  rusgraprop  24929  rusgraprop3  24943  frgranbnb  25020  frgrancvvdeqlem3  25032  frgrancvvdeqlem4  25033  frgrancvvdeqlem7  25036  frgrawopreglem2  25045  frgrawopreg  25049  frgregordn0  25070  clwwlkextfrlem1  25076  extwwlkfablem2  25078  numclwwlkun  25079  numclwwlkovf2ex  25086  numclwlk1lem2foa  25091  numclwlk1lem2f1  25094  numclwwlk8  25115  gxid  25275  opidonOLD  25324  opidon2OLD  25326  grpomndo  25348  elghomlem2OLD  25364  rngoueqz  25432  dvrunz  25435  rngoridfz  25437  hlipgt0  25830  ocin  26214  ocnel  26216  shmodsi  26307  pjmf1  26634  unopf1o  26835  staddi  27165  stadd3i  27167  mdi  27214  dmdmd  27219  dmdi  27221  dmdbr2  27222  dmdbr3  27224  dmdbr4  27225  dmdi4  27226  mdsl1i  27240  superpos  27273  cvbr4i  27286  atssma  27297  atcv1  27299  atomli  27301  chirredlem1  27309  addltmulALT  27365  bian1d  27366  ifeqeqx  27419  disjxpin  27447  suppss3  27550  fpwrelmap  27556  xrge0infss  27580  ogrpaddlt  27708  metider  27873  tpr2rico  27894  xrge0iifiso  27917  qqhcn  27972  qqhucn  27973  esumlub  28068  esumpinfval  28079  esumpinfsum  28083  ballotlemfc0  28431  ballotlemfcc  28432  erdsze2lem2  28648  trpredrec  29321  poseq  29333  soseq  29334  sltval2  29416  sltres  29424  nodenselem7  29447  nodenselem8  29448  nodense  29449  nobndup  29460  nobnddown  29461  nofulllem5  29466  dfrdg4  29600  altopthsn  29611  btwncomim  29663  btwnexch3  29670  btwnexch2  29673  endofsegid  29735  onsuct0  29906  ordcmp  29912  nndivsub  29922  wl-equsal1i  29996  wl-ax11-lem10  30034  ltflcei  30043  sin2h  30045  cos2h  30046  tan2h  30047  heicant  30049  mblfinlem1  30051  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  mbfresfi  30061  cnambfre  30063  dvtanlem  30064  ftc1anc  30098  dvasin  30103  areacirclem1  30107  areacirclem4  30110  areacirc  30112  opnrebl2  30139  nn0prpwlem  30140  brabg2  30206  fzmul  30233  fdc  30238  incsequz2  30242  isbnd2  30279  divrngidl  30425  rexrabdioph  30727  fphpdo  30751  icodiamlt  30756  irrapxlem3  30760  rmxypairf1o  30847  rmxycomplete  30853  zindbi  30882  lermxnn0  30888  ltrmy  30890  rmyeq0  30891  rmyeq  30892  lermy  30893  acongsym  30914  acongneg2  30915  wepwsolem  30987  radcnvrat  31195  nzss  31222  expgrowthi  31238  ordpss  31360  fzisoeu  31500  climinf  31612  stoweidlem7  31789  stoweidlem62  31844  2reu3  32193  ralbinrald  32204  funressnfv  32213  afv0fv0  32234  afv0nbfvbi  32236  afvfv0bi  32237  fnbrafvb  32239  afvres  32257  tz6.12-afv  32258  afvco2  32261  ndmaovcl  32288  f1dmvrnfibi  32312  zm1nn  32325  subsubelfzo0  32338  usgra2pth  32354  usgpredgv  32399  usgpredgvALT  32400  usgfis  32446  usgfisALT  32450  mgmpropd  32463  clintop  32532  isassintop  32534  isinitoi  32609  istermoi  32610  iszeroi  32615  funcestrcsetclem8  32653  fthestrcsetc  32656  funcsetcestrclem8  32668  fthsetcestrc  32671  lidldomn1  32727  uzlidlring  32735  2zrngnmlid2  32757  rngccatidOLD  32797  ringccatidOLD  32860  srhmsubc  32884  srhmsubcOLD  32903  ztprmneprm  32936  pgrpgt2nabl  32959  lindslinindimp2lem4  33062  lincresunit3  33082  bi23impib  33254  bi23imp13  33260  bitr3  33280  rspsbc2  33305  tratrb  33307  sbcim2g  33309  truniALT  33312  3impcombi  33614  tpid3gVD  33642  orbi1rVD  33648  sbc3orgVD  33651  rspsbc2VD  33655  tratrbVD  33661  sbcim2gVD  33675  sbcbiVD  33676  truniALTVD  33678  trintALTVD  33680  trintALT  33681  csbingVD  33684  csbsngVD  33693  csbxpgVD  33694  csbresgVD  33695  csbrngVD  33696  csbima12gALTVD  33697  csbunigVD  33698  csbfv12gALTVD  33699  relopabVD  33701  isosctrlem1ALT  33734  bnj517  33943  bj-cbvexw  34235  bj-cbv3tb  34271  bj-spimtv  34278  bj-spvv  34284  bj-chvarv  34286  bj-cbvalv  34296  bj-cleqh  34358  bj-equsal  34399  bj-ax8  34461  bj-vtoclf  34480  bj-snsetex  34521  bj-inftyexpiinj  34612  bj-finsumval0  34663  bj-bary1lem1  34680  bj-bary1  34681  lsatn0  34724  l1cvpat  34779  leat2  35019  atnle  35042  cvlcvr1  35064  cvrexchlem  35143  cvratlem  35145  cvrat  35146  atcvrj0  35152  atle  35160  snatpsubN  35474  linepsubN  35476  pmapsub  35492  lneq2at  35502  lncvrelatN  35505  2llnma3r  35512  cdlemblem  35517  paddasslem5  35548  poml4N  35677  lhpmcvr4N  35750  trlval2  35888  cdlemd6  35928  cdleme7ga  35973  cdleme25b  36080  cdleme29b  36101  cdleme35fnpq  36175  cdleme50f1  36269  cdlemf1  36287  cdlemg27b  36422  cdlemk28-3  36634  tendospcanN  36750  diaf11N  36776  dia2dimlem1  36791  dibf11N  36888  dihf11  36994  dihmeetlem1N  37017  dochvalr  37084  dochnel2  37119  dvh4dimlem  37170  dochsat0  37184  mapd1o  37375  hdmapf1oN  37595  hgmapval0  37622  hgmapf1oN  37633  hlhilhillem  37690  axfrege52a  37883  axfrege52c  37914  suprleubrd  37983  suprlubrd  37987
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
  Copyright terms: Public domain W3C validator