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

Theorem biimpi 197
Description: Infer an implication from a logical equivalence. Inference associated with biimp 196. (Contributed by NM, 29-Dec-1992.)
Hypothesis
Ref Expression
biimpi.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
biimpi  |-  ( ph  ->  ps )

Proof of Theorem biimpi
StepHypRef Expression
1 biimpi.1 . 2  |-  ( ph  <->  ps )
2 biimp 196 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
31, 2ax-mp 5 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  sylbi  198  sylib  199  sylbb  200  biimpri  209  mpbi  211  syl5bi  220  syl6ib  229  syl7bi  233  syl8ib  234  pm2.53  374  simplbi  461  simprbi  465  sylanb  474  sylan2b  477  pm3.1  500  orbi2i  521  pm2.32  528  anc2l  557  pm3.37  581  dfbi  633  pm2.76  856  pm5.15  897  pm5.16  898  pm5.75  945  rnlemOLD  973  simp1bi  1020  simp2bi  1021  simp3bi  1022  syl3an1b  1300  syl3an2b  1301  syl3an3b  1302  nic-ax  1550  19.25  1737  stdpc5vOLD  1781  sbbii  1797  spvw  1807  excomim  1905  stdpc5  1967  sb9i  2232  exmoeu  2308  2mo  2357  eqeq1d  2430  gencbvex  3067  moeq  3189  euind  3200  reuind  3218  eqsbc3r  3299  ra4v  3327  ra4  3329  ssel  3401  elunnel1  3550  unssd  3585  ssind  3629  n0moeu  3718  ss0  3738  uneqdifeq  3829  rabsnif  4012  prprc  4055  ssunsn2  4102  eqsn  4104  unisn2  4503  snexALT  4553  reusv3i  4574  snex  4605  brrelex12  4834  elrel  4899  exopxfr2  4941  dmxp  5015  xpssres  5101  elres  5102  elimasni  5157  inisegn0  5162  xpdifid  5227  dmsnsnsn  5276  coi2  5314  xpco  5338  iotabi  5517  uniabio  5518  iotaint  5521  nfunv  5575  funun  5586  funcnv3  5605  funimass1  5617  funssxp  5702  f0dom0  5727  f1o00  5807  dffv3  5821  dffv2  5898  fndmin  5948  iinpreima  5969  fveqressseq  5977  fsn2  6021  ftpg  6033  f12dfv  6131  f13dfv  6132  nvocnv  6139  isoselem  6191  riotaxfrd  6241  oprabid  6276  mpt2difsnif  6347  ovima0  6406  sorpsscmpl  6540  unexg  6550  ordsson  6574  peano2  6671  1stval  6753  2ndval  6754  1stdm  6798  oprabco  6835  f1o2ndf1  6859  poxp  6863  suppval1  6875  funsssuppss  6896  fnsuppeq0  6898  imacosupp  6910  wfrlem4  6994  wfrlem5  6995  wfrlem10  7000  wfrlem15  7005  tz7.49c  7118  undifixp  7513  bren2  7554  ensym  7572  en1uniel  7595  domunsn  7675  limenpsi  7700  php4  7712  snnen2o  7714  isinf  7738  en2  7760  findcard2  7764  unfilem1  7788  suppssfifsupp  7851  fsuppunbi  7857  elfiun  7897  marypha1lem  7900  marypha2lem3  7904  supval2  7922  supmaxlemOLD  7935  eqinf  7953  brwdom2  8041  brwdom3  8050  sucprcreg  8067  preleq  8075  tcmin  8177  prwf  8234  r1pw  8268  rankuni2b  8276  rankr1id  8285  cardval3  8338  ficardom  8347  cardmin2  8384  isinfcard  8474  iscard3  8475  alephval3  8492  dfac9  8517  kmlem6  8536  ackbij1lem12  8612  fin23lem29  8722  fin23lem30  8723  fin23lem41  8733  isf32lem11  8744  isfin1-3  8767  fin1a2lem11  8791  fin1a2lem12  8792  fin1a2lem13  8793  axcc2lem  8817  dominf  8826  axdc4lem  8836  dominfac  8949  pwcfsdom  8959  cfpwsdom  8960  tskuni  9159  wfgru  9192  rpregt0  11266  supxrun  11552  elicore  11638  xrge0neqmnf  11688  elfz1end  11780  1fv  11859  elfzonlteqm1  11939  fzennn  12131  cardfz  12133  fsuppmapnn0fiubex  12154  fsuppmapnn0fiub0  12155  ser0  12215  crreczi  12347  faclbnd  12425  bcn1  12448  hashrabsn01  12502  hashge0  12516  hashssdif  12537  hashsnlei  12540  hashpw  12556  ccatw2s1p1  12715  swrd0len0  12738  swrdtrcfv  12743  swrdswrd  12762  swrdccatwrd  12770  swrdccatin2  12789  swrdccat3  12794  swrdccat3a  12796  repsundef  12820  cshwlen  12847  s4f1o  12947  trclublem  13003  reltrclfv  13025  dmtrclfv  13026  relexpsucnnr  13032  sqrt0  13249  cau3lem  13361  harmonic  13860  mertenslem2  13884  prodf1  13890  fprodfac  13970  fprodle  13993  risefacp1  14025  fallfacp1  14026  rpnnen2  14221  lcmcllem  14504  lcmftp  14552  lcmfunsnlem2lem1  14554  lcmfunsnlem2lem2  14555  prmind2  14578  ncoprmgcdne1b  14598  coprmproddvdslem  14622  pceq0  14763  prmreclem6  14808  0ram  14921  ram0  14923  cshwsdisj  15012  cshwsiun  15013  ressbas2  15123  ressinbas  15128  ressval3d  15129  mrcuni  15470  mreexexlem4d  15496  catpropd  15557  initoid  15843  termoid  15844  initoeu2lem0  15851  arwhoma  15883  joinfval  16190  meetfval  16204  clatlem  16300  lubun  16312  psssdm  16405  ismgmn0  16433  plusfeq  16438  isnsgrp  16474  isnmnd  16483  grpissubg  16780  idrespermg  16995  symgextfv  17002  fvcosymgeq  17013  pmtrprfv3  17038  pmtr3ncomlem1  17057  psgnunilem4  17081  gsummptfzsplitl  17509  gsumzoppg  17520  gsum2dlem1  17545  gsum2dlem2  17546  gsum2d  17547  srg1zr  17705  staffn  18020  scafeq  18054  lbsexg  18330  lidldvgen  18422  ply1bascl2  18740  cply1mul  18830  lply1binom  18843  prmirred  19008  zlmassa  19037  frgpcyg  19086  ipfeq  19159  dsmmbas2  19242  frlmbas3  19276  mamufacex  19356  matsubgcell  19401  matinvgcell  19402  matvscacell  19403  mpt2matmul  19413  matepmcl  19429  matepm2cl  19430  mat1dimbas  19439  scmatscm  19480  smatvscl  19491  marrepcl  19531  marepvcl  19536  mulmarep1el  19539  mulmarep1gsum1  19540  mulmarep1gsum2  19541  submabas  19545  nfimdetndef  19556  mdetfval1  19557  m1detdiag  19564  mdetdiag  19566  mdetunilem7  19585  mdetunilem9  19587  m2detleib  19598  gsummatr01lem3  19624  smadiadetlem4  19636  slesolinv  19647  slesolinvbi  19648  slesolex  19649  cramerimplem2  19651  pmatcoe1fsupp  19667  mat2pmatbas  19692  mat2pmatmul  19697  mat2pmatlin  19701  m2cpminvid2lem  19720  decpmatmul  19738  monmatcollpw  19745  pmatcollpw3fi  19751  pm2mpf1  19765  pm2mpghm  19782  fvmptnn04ifb  19817  cayhamlem1  19832  isbasis3g  19906  isopn2  19989  ntrval2  20008  toponmre  20051  innei  20083  restcld  20130  restcldi  20131  neitr  20138  discmp  20355  cmpsublem  20356  cmpsub  20357  2ndcctbss  20412  ssref  20469  lfinun  20482  dissnref  20485  ptcnp  20579  imasnopn  20647  imasncld  20648  imasncls  20649  kqf  20704  fbun  20797  opnfbas  20799  supfil  20852  ufprim  20866  acufl  20874  filufint  20877  ufldom  20919  hausflf2  20955  alexsubALTlem4  21007  cnextfval  21019  cnextfun  21021  cnextfres1  21025  trust  21186  utoptop  21191  ustuqtop1  21198  metustid  21511  metustfbas  21514  cfilucfil  21516  metustbl  21523  restmetu  21527  zlmclm  22068  cphassr  22131  ovolun  22394  volun  22440  vitalilem2  22509  dvmptfsum  22869  rolle  22884  ulmcaulem  23291  logfac  23492  logno1  23523  logreclem  23641  cxplogb  23665  leibpilem1  23808  prmorcht  24047  pclogsum  24085  2sqlem10  24244  chto1lb  24258  tgldimor  24488  axcontlem7  24942  usgraop  25019  ausisusgra  25024  usgra2edg1  25052  usgrarnedg  25053  usgraedg4  25056  usgra1v  25059  usgraidx2vlem2  25061  usgraidx2v  25062  usgrares1  25080  nbgrassvwo  25107  nbgrassvwo2  25108  nb3graprlem2  25122  nb3grapr  25123  nb3grapr2  25124  nb3gra2nb  25125  cusgra3v  25134  cusgrafilem2  25150  usgrasscusgra  25153  uvtxnbgra  25163  uvtxnb  25167  2trllemH  25224  2trllemE  25225  constr1trl  25260  usgra2adedgwlkonALT  25286  usgra2wlkspthlem2  25290  fargshiftfo  25308  wwlknndef  25407  wwlkextproplem3  25413  clwlkswlks  25428  clwwlknndef  25443  clwlkisclwwlklem2a4  25454  clwlkisclwwlklem1  25457  clwwlkf  25464  clwwlkvbij  25471  wwlkext2clwwlk  25473  clwwnisshclwwn  25479  erclwwlkref  25483  erclwwlknref  25495  erclwwlknsym  25496  erclwwlkntr  25497  hashecclwwlkn1  25504  usghashecclwwlk  25505  clwlkfoclwwlk  25515  el2wlkonot  25539  el2spthonot  25540  el2wlkonotot0  25542  vdgrnn0pnf  25579  clwlknclwlkdifs  25630  eupatrl  25638  frgra3v  25672  3vfriswmgra  25675  1to3vfriswmgra  25677  1to3vfriendship  25678  2pthfrgra  25681  4cycl2v2nb  25686  n4cyclfrgra  25688  frgranbnb  25690  frgrancvvdeqlem4  25703  frgrawopreg  25719  frg2woteqm  25729  usg2spot2nb  25735  numclwwlkovf2ex  25756  numclwwlk3lem  25778  grpoidinvlem3  25876  nmlno0lem  26376  blocni  26388  pythi  26433  normpythi  26737  shmodsi  26984  omlsilem  26997  pjchi  27027  chlubii  27067  osumi  27237  nmlnop0iALT  27590  cnlnssadj  27675  nmopcoi  27690  mdbr3  27892  mdbr4  27893  ssmd1  27906  dmdsl3  27910  mdslmd1lem2  27921  mdslmd4i  27928  mdexchi  27930  atssma  27973  atoml2i  27978  chirredlem3  27987  mdsymlem1  27998  mdsymlem3  28000  dmdbr6ati  28018  dmdbr7ati  28019  cdjreui  28027  cdj3lem2b  28032  addltmulALT  28041  ssrmo  28072  difuncomp  28112  iundifdif  28124  imadifxp  28158  fresf1o  28177  fimacnvinrn2  28182  sspreima  28192  acunirnmpt  28207  acunirnmpt2  28208  aciunf1lem  28210  aciunf1  28211  disjdsct  28229  1stpreimas  28232  resf1o  28265  xrge0addge  28287  xlt2addrd  28288  xrge0infssOLD  28291  f1ocnt  28326  ressmulgnn0  28397  xrge0nre  28404  gsummpt2co  28494  gsummpt2d  28495  kerunit  28538  pmtrprfv2  28563  psgnfzto1stlem  28565  fzto1st  28568  psgnfzto1st  28570  submat1n  28583  submatres  28584  lmat22lem  28595  locfinreflem  28619  ldlfcntref  28633  pstmfval  28651  mndpluscn  28684  rge0scvg  28707  pnfneige0  28709  pl1cn  28713  nexple  28783  indval2  28788  gsumesum  28832  esumcst  28836  esumrnmpt2  28841  esumcvgsum  28861  esumgect  28863  esumcvgre  28864  esum2d  28866  esumiun  28867  pwsiga  28904  insiga  28911  elsigagen2  28922  inelpisys  28928  sigapisys  28929  unelldsys  28932  ldsysgenld  28934  measxun2  28984  volmeas  29006  ddemeas  29011  aean  29019  mbfmfun  29028  mbfmbfm  29032  1stmbfm  29034  2ndmbfm  29035  omsfval  29070  omsfvalOLD  29074  oms0  29077  omssubadd  29080  oms0OLD  29081  omssubaddOLD  29084  carsgclctunlem1  29101  sibfof  29125  eulerpartlemt  29156  eulerpartlemmf  29160  eulerpartlemgs2  29165  probun  29204  dstfrvclim1  29262  coinfliprv  29267  ballotlem2  29273  ballotlemfp1  29276  ballotlemic  29291  ballotlem1c  29292  ballotlemicOLD  29329  ballotlem1cOLD  29330  plymulx0  29388  signsvtn0  29411  signstres  29416  bnj529  29503  bnj927  29532  bnj1379  29594  bnj1424  29602  bnj1436  29603  bnj1476  29610  bnj607  29679  bnj908  29694  bnj1097  29742  bnj1118  29745  bnj1128  29751  bnj1145  29754  bnj1154  29760  bnj1174  29764  bnj1189  29770  bnj1204  29773  bnj1388  29794  bnj1417  29802  cvmliftlem10  29969  mrsub0  30106  mrsubccat  30108  mrsubcn  30109  ghomgrpilem2  30256  bcprod  30325  bccolsum  30326  faclim  30333  dfon2lem3  30382  dfon2lem7  30386  dfon2lem8  30387  rdgprc0  30391  frrlem4  30468  frrlem5  30469  fvsingle  30636  unisnif  30641  funpartlem  30658  hfun  30894  trer  30921  clsun  30933  opnregcld  30935  cldregopn  30936  fnessref  30962  df3nandALT1  31006  lukshef-ax2  31024  nandsym1  31031  sylancl2  31111  bj-gl4  31127  bj-babygodel  31135  bj-babylob  31136  bj-alrimhi  31157  bj-nfext  31212  bj-ax9  31409  bj-snsetex  31468  bj-1upln0  31514  bj-inftyexpidisj  31559  bj-elccinfty  31563  finixpnum  31837  fin2so  31839  poimirlem9  31856  poimirlem13  31860  poimirlem14  31861  poimirlem25  31872  poimirlem26  31873  mblfinlem2  31885  mblfinlem3  31886  mblfinlem4  31887  ismblfin  31888  mbfresfi  31894  ftc1cnnc  31923  ftc1anclem6  31929  dvasin  31935  fnopabco  31956  frinfm  31969  nninfnub  31987  caushft  31997  bndss  32025  ispridl2  32178  notornotel1  32238  tsbi2  32283  abeq12  32306  rabeq12f  32307  axc11n-16  32421  lkr0f  32572  glbconN  32854  paddssat  33291  pclunN  33375  2polssN  33392  paddunN  33404  poldmj1N  33405  ltrnnid  33613  dibglbN  34646  istopclsd  35454  pellex  35592  monotoddzzfi  35703  jm2.23  35764  expdioph  35791  dford3lem1  35794  wopprc  35798  kelac1  35834  dfac21  35837  lsmfgcl  35845  pwssplit4  35860  isnumbasgrp  35879  dgraalem  35920  dgraalemOLD  35921  ifpbi1  36034  rp-fakeanorass  36070  rp-isfinite5  36075  superficl  36084  ssuncl  36087  sssymdifcl  36089  relintab  36102  cnvssb  36105  cotrintab  36134  clcnvlem  36143  cnvtrrel  36175  brfvrcld2  36197  relexpxpmin  36222  relexpaddss  36223  brtrclfv2  36232  unhe1  36294  frege55lem1b  36404  frege58bid  36411  frege92  36464  imadisjlnd  36512  bcc0  36602  pm10.12  36620  pm11.61  36656  sbiota1  36698  bi1imp  36750  bi2imp  36751  bi3impb  36752  bi3impa  36753  bi13impib  36755  bi123impib  36756  bi13impia  36757  bi123impia  36758  bi13imp23  36761  bi13imp2  36762  bi12imp3  36763  dfvd1imp  36859  dfvd2imp  36896  e1bi  36922  e2bi  36925  e3bi  37041  3ornot23VD  37159  3impexpbicomVD  37169  3impexpbicomiVD  37170  tratrbVD  37174  ssralv2VD  37179  equncomiVD  37182  truniALTVD  37191  ee33VD  37192  csbingVD  37197  onfrALTlem3VD  37200  onfrALTlem2VD  37202  onfrALTlem1VD  37203  onfrALTVD  37204  csbsngVD  37206  csbxpgVD  37207  csbrngVD  37209  csbunigVD  37211  csbfv12gALTVD  37212  relopabVD  37214  2uasbanhVD  37224  vk15.4jVD  37227  unisnALT  37239  chordthmALT  37246  iunconlem2  37248  fnchoice  37266  elunnel2  37276  pwssfi  37297  uzwo4  37308  inabs3  37312  suprnmpt  37342  wessf1ornlem  37363  disjrnmpt2  37367  founiiun0  37369  disjf1o  37370  fompt  37371  disjinfi  37372  fzisoeu  37415  upbdrech  37420  ssfiunibd  37424  iuneqfzuzlem  37454  iuneqfzuz  37455  xrge0ge0  37467  xrssre  37468  infrpge  37471  eliocre  37501  lbioc  37506  fsumiunss  37538  fmuldfeq  37544  infrglbOLD  37552  mccl  37561  climsuselem1  37569  climsuse  37570  ellimcabssub0  37580  islptre  37582  lptioo2  37594  lptioo1  37595  islpcn  37602  icccncfext  37648  cncfiooicclem1  37654  cncfiooicc  37655  cncfioobdlem  37657  dvbdfbdioo  37685  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  dvnprodlem1  37704  dvnprodlem2  37705  dvnprodlem3  37706  volioc  37732  itgioocnicc  37737  stoweidlem28  37771  stoweidlem52  37796  stoweidlem57  37801  wallispilem3  37812  wallispilem4  37813  wallispi  37815  wallispi2lem1  37816  wallispi2lem2  37817  wallispi2  37818  stirlinglem7  37825  stirlinglem10  37828  stirlinglem12  37830  fourierdlem12  37864  fourierdlem20  37872  fourierdlem25  37877  fourierdlem33  37886  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem48  37901  fourierdlem50  37903  fourierdlem52  37905  fourierdlem57  37910  fourierdlem58  37911  fourierdlem59  37912  fourierdlem65  37918  fourierdlem68  37921  fourierdlem70  37923  fourierdlem71  37924  fourierdlem73  37926  fourierdlem74  37927  fourierdlem75  37928  fourierdlem76  37929  fourierdlem80  37933  fourierdlem93  37946  fourierdlem101  37954  fourierdlem103  37956  fourierdlem104  37957  fourierswlem  37977  fouriersw  37978  etransclem26  38008  etransclem37  38019  saluncl  38042  salgenval  38046  intsaluni  38052  intsal  38053  salgencl  38054  sge00  38069  sge0sn  38072  sge0cl  38074  sge0f1o  38075  sge0less  38085  sge0rnbnd  38086  sge0pnffigt  38089  sge0lefi  38091  sge0ltfirp  38093  sge0resplit  38099  sge0split  38102  sge0iunmptlemfi  38106  sge0iunmptlemre  38108  sge0fodjrnlem  38109  sge0iunmpt  38111  sge0isum  38120  sge0xp  38122  sge0xaddlem2  38127  iundjiun  38149  meadjun  38151  meassle  38152  meadjiunlem  38154  ismeannd  38156  meaiunlelem  38157  psmeasure  38160  carageneld  38174  caragenunidm  38180  omeunle  38188  omeiunltfirp  38191  caratheodorylem1  38198  caratheodory  38200  icoresmbl  38212  volicorescl  38222  ovncvrrp  38233  ovnsubaddlem2  38240  hoidmv1lelem1  38260  hoidmv1le  38263  hoidmvlelem1  38264  hoidmvlelem2  38265  hoidmvlelem3  38266  hoidmvlelem5  38268  hoidmvle  38269  ovnhoilem2  38271  aifftbifffaibif  38323  aifftbifffaibifff  38324  abciffcbatnabciffncba  38331  abciffcbatnabciffncbai  38332  nabctnabc  38333  confun4  38344  confun5  38345  plcofph  38346  pldofph  38347  plvcofph  38348  plvcofphax  38349  plvofpos  38350  dandysum2p2e4  38400  2reu4a  38424  ndmaovrcl  38519  iccpartiun  38561  iccpartdisj  38564  dfodd5  38602  stgoldbwt  38690  nnsum3primesle9  38702  nnsum4primesodd  38704  nnsum4primesoddALTV  38705  nnsum4primeseven  38708  pfxccat3  38780  pfxccatpfx1  38781  elpwdifsn  38799  pr1eqbg  38800  propeqop  38808  edgupgr  38988  ausgrusgrb  39010  ausgrumgri  39012  usgridx2vlem2  39050  usgridx2v  39051  usgredgedga  39054  umgrres1lem  39114  upgrres1  39117  usgr1v0e  39128  dfnbgr3  39144  nbgrnvtx0  39145  nbgrel  39146  nbuhgr  39147  nbuhgr2vtx1edgb  39156  nbgrssvwo2  39169  edgnbusgreu  39177  nbusgrf1o0  39179  nb3grprlem2  39186  nb3grpr2  39188  nb3gr2nb  39189  cusgredg  39220  cplgr2vpr  39228  cplgr3v  39230  usgra2pthlem1  39258  usgra2pth  39259  usgvincvad  39307  usgvincvadALT  39310  usg2edgneu  39315  usgedgvadf1lem2  39317  usgedgvadf1  39318  usgedgvadf1ALTlem2  39320  usgedgvadf1ALT  39321  usgo0s0  39338  usgo0s0ALT  39339  usgo1s0ALT  39340  usgrafisbaseALT  39343  usgrafisbaseALT2  39344  usgo1s0  39345  usgfis  39349  usgfisALT  39353  lmod0rng  39459  lidldomnnring  39521  fdmdifeqresdif  39716  altgsumbcALT  39727  ply1sclrmsm  39768  lcoop  39797  lincfsuppcl  39799  linccl  39800  lincvalsng  39802  lincvalpr  39804  lincvalsc0  39807  linc0scn0  39809  lincdifsn  39810  linc1  39811  lincsum  39815  lincscm  39816  lindslinindsimp2lem5  39848  snlindsntor  39857  lincresunit3lem2  39866  ldepsnlinclem1  39891  ldepsnlinclem2  39892  difmodm1lt  39918  nn0sumshdiglemB  40024
  Copyright terms: Public domain W3C validator