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  1552  19.25  1735  stdpc5vOLD  1777  sbbii  1793  spvw  1803  excomim  1900  stdpc5  1962  sb9i  2219  exmoeu  2296  2mo  2345  2moOLD  2346  eqeq1d  2422  eqeq1OLD  2425  eleq2OLD  2495  gencbvex  3122  moeq  3244  euind  3255  reuind  3272  eqsbc3r  3353  ra4v  3381  ra4  3383  ssel  3455  elunnel1  3604  unssd  3639  ssind  3683  n0moeu  3772  ss0  3790  uneqdifeq  3881  rabsnif  4063  prprc  4106  ssunsn2  4153  eqsn  4155  unisn2  4552  snexALT  4602  reusv3i  4623  snex  4654  brrelex12  4883  elrel  4948  exopxfr2  4990  dmxp  5064  xpssres  5150  elres  5151  elimasni  5206  inisegn0  5211  xpdifid  5276  dmsnsnsn  5325  coi2  5363  xpco  5387  iotabi  5565  uniabio  5566  iotaint  5569  nfunv  5623  funun  5634  funcnv3  5653  funimass1  5665  funssxp  5750  f0dom0  5775  f1o00  5854  dffv3  5868  dffv2  5945  fndmin  5995  iinpreima  6016  fveqressseq  6024  fsn2  6068  ftpg  6080  f12dfv  6178  f13dfv  6179  nvocnv  6186  isoselem  6238  riotaxfrd  6288  oprabid  6323  mpt2difsnif  6394  ovima0  6453  sorpsscmpl  6587  unexg  6597  ordsson  6621  peano2  6718  1stval  6800  2ndval  6801  1stdm  6845  oprabco  6882  f1o2ndf1  6906  poxp  6910  suppval1  6922  funsssuppss  6943  fnsuppeq0  6945  imacosupp  6957  wfrlem4  7038  wfrlem5  7039  wfrlem10  7044  wfrlem15  7049  tz7.49c  7162  undifixp  7557  bren2  7598  ensym  7616  en1uniel  7639  domunsn  7719  limenpsi  7744  php4  7756  snnen2o  7758  isinf  7782  en2  7804  findcard2  7808  unfilem1  7832  suppssfifsupp  7895  fsuppunbi  7901  elfiun  7941  marypha1lem  7944  marypha2lem3  7948  supval2  7966  supmaxlemOLD  7979  eqinf  7997  brwdom2  8079  brwdom3  8088  sucprcreg  8105  preleq  8113  tcmin  8215  prwf  8272  r1pw  8306  rankuni2b  8314  rankr1id  8323  cardval3  8376  ficardom  8385  cardmin2  8422  isinfcard  8512  iscard3  8513  alephval3  8530  dfac9  8555  kmlem6  8574  ackbij1lem12  8650  fin23lem29  8760  fin23lem30  8761  fin23lem41  8771  isf32lem11  8782  isfin1-3  8805  fin1a2lem11  8829  fin1a2lem12  8830  fin1a2lem13  8831  axcc2lem  8855  dominf  8864  axdc4lem  8874  dominfac  8987  pwcfsdom  8997  cfpwsdom  8998  tskuni  9197  wfgru  9230  rpregt0  11304  supxrun  11590  elicore  11676  elfz1end  11816  1fv  11895  elfzonlteqm1  11975  fzennn  12167  cardfz  12169  fsuppmapnn0fiubex  12190  fsuppmapnn0fiub0  12191  ser0  12251  crreczi  12383  faclbnd  12461  bcn1  12484  hashrabsn01  12538  hashge0  12552  hashssdif  12573  hashsnlei  12576  hashpw  12592  hash2prd  12616  ccatw2s1p1  12743  swrd0len0  12766  swrdtrcfv  12771  swrdswrd  12790  swrdccatwrd  12798  swrdccatin2  12817  swrdccat3  12822  swrdccat3a  12824  repsundef  12848  cshwlen  12875  s4f1o  12971  trclublem  13027  reltrclfv  13049  dmtrclfv  13050  relexpsucnnr  13056  sqrt0  13273  cau3lem  13385  harmonic  13884  mertenslem2  13908  prodf1  13914  fprodfac  13994  fprodle  14017  risefacp1  14049  fallfacp1  14050  rpnnen2  14245  lcmcllem  14521  lcmftp  14569  lcmfunsnlem2lem1  14571  lcmfunsnlem2lem2  14572  prmind2  14595  ncoprmgcdne1b  14615  coprmproddvdslem  14639  pceq0  14772  prmreclem6  14817  0ram  14930  ram0  14932  cshwsdisj  15021  cshwsiun  15022  ressbas2  15132  ressinbas  15137  ressval3d  15138  mrcuni  15471  mreexexlem4d  15497  catpropd  15558  initoid  15844  termoid  15845  initoeu2lem0  15852  arwhoma  15884  joinfval  16191  meetfval  16205  clatlem  16301  lubun  16313  psssdm  16406  ismgmn0  16434  plusfeq  16439  isnsgrp  16475  isnmnd  16484  grpissubg  16781  idrespermg  16996  symgextfv  17003  fvcosymgeq  17014  pmtrprfv3  17039  pmtr3ncomlem1  17058  psgnunilem4  17082  gsummptfzsplitl  17494  gsumzoppg  17505  gsum2dlem1  17530  gsum2dlem2  17531  gsum2d  17532  srg1zr  17690  staffn  18005  scafeq  18039  lbsexg  18315  lidldvgen  18407  ply1bascl2  18725  cply1mul  18815  lply1binom  18828  prmirred  18990  zlmassa  19019  frgpcyg  19068  ipfeq  19141  dsmmbas2  19224  frlmbas3  19258  mamufacex  19338  matsubgcell  19383  matinvgcell  19384  matvscacell  19385  mpt2matmul  19395  matepmcl  19411  matepm2cl  19412  mat1dimbas  19421  scmatscm  19462  smatvscl  19473  marrepcl  19513  marepvcl  19518  mulmarep1el  19521  mulmarep1gsum1  19522  mulmarep1gsum2  19523  submabas  19527  nfimdetndef  19538  mdetfval1  19539  m1detdiag  19546  mdetdiag  19548  mdetunilem7  19567  mdetunilem9  19569  m2detleib  19580  gsummatr01lem3  19606  smadiadetlem4  19618  slesolinv  19629  slesolinvbi  19630  slesolex  19631  cramerimplem2  19633  pmatcoe1fsupp  19649  mat2pmatbas  19674  mat2pmatmul  19679  mat2pmatlin  19683  m2cpminvid2lem  19702  decpmatmul  19720  monmatcollpw  19727  pmatcollpw3fi  19733  pm2mpf1  19747  pm2mpghm  19764  fvmptnn04ifb  19799  cayhamlem1  19814  isbasis3g  19888  isopn2  19971  ntrval2  19990  toponmre  20033  innei  20065  restcld  20112  restcldi  20113  neitr  20120  discmp  20337  cmpsublem  20338  cmpsub  20339  2ndcctbss  20394  ssref  20451  lfinun  20464  dissnref  20467  ptcnp  20561  imasnopn  20629  imasncld  20630  imasncls  20631  kqf  20686  fbun  20779  opnfbas  20781  supfil  20834  ufprim  20848  acufl  20856  filufint  20859  ufldom  20901  hausflf2  20937  alexsubALTlem4  20989  cnextfval  21001  cnextfun  21003  cnextfres1  21007  trust  21168  utoptop  21173  ustuqtop1  21180  metustid  21493  metustfbas  21496  cfilucfil  21498  metustbl  21505  restmetu  21509  zlmclm  22012  cphassr  22075  ovolun  22326  volun  22372  vitalilem2  22441  dvmptfsum  22801  rolle  22816  ulmcaulem  23211  logfac  23412  logno1  23443  logreclem  23561  cxplogb  23585  leibpilem1  23728  prmorcht  23965  pclogsum  24003  2sqlem10  24162  chto1lb  24176  tgldimor  24406  axcontlem7  24843  usgraop  24920  ausisusgra  24925  usgra2edg1  24953  usgrarnedg  24954  usgraedg4  24957  usgra1v  24960  usgraidx2vlem2  24962  usgraidx2v  24963  usgrares1  24980  nbgrassvwo  25007  nbgrassvwo2  25008  nb3graprlem2  25022  nb3grapr  25023  nb3grapr2  25024  nb3gra2nb  25025  cusgra3v  25034  cusgrafilem2  25050  usgrasscusgra  25053  uvtxnbgra  25063  uvtxnb  25067  2trllemH  25124  2trllemE  25125  constr1trl  25160  usgra2adedgwlkonALT  25186  usgra2wlkspthlem2  25190  fargshiftfo  25208  wwlknndef  25307  wwlkextproplem3  25313  clwlkswlks  25328  clwwlknndef  25343  clwlkisclwwlklem2a4  25354  clwlkisclwwlklem1  25357  clwwlkf  25364  clwwlkvbij  25371  wwlkext2clwwlk  25373  clwwnisshclwwn  25379  erclwwlkref  25383  erclwwlknref  25395  erclwwlknsym  25396  erclwwlkntr  25397  hashecclwwlkn1  25404  usghashecclwwlk  25405  clwlkfoclwwlk  25415  el2wlkonot  25439  el2spthonot  25440  el2wlkonotot0  25442  vdgrnn0pnf  25479  clwlknclwlkdifs  25530  eupatrl  25538  frgra3v  25572  3vfriswmgra  25575  1to3vfriswmgra  25577  1to3vfriendship  25578  2pthfrgra  25581  4cycl2v2nb  25586  n4cyclfrgra  25588  frgranbnb  25590  frgrancvvdeqlem4  25603  frgrawopreg  25619  frg2woteqm  25629  usg2spot2nb  25635  numclwwlkovf2ex  25656  numclwwlk3lem  25678  grpoidinvlem3  25776  nmlno0lem  26276  blocni  26288  pythi  26333  normpythi  26627  shmodsi  26874  omlsilem  26887  pjchi  26917  chlubii  26957  osumi  27127  nmlnop0iALT  27480  cnlnssadj  27565  nmopcoi  27580  mdbr3  27782  mdbr4  27783  ssmd1  27796  dmdsl3  27800  mdslmd1lem2  27811  mdslmd4i  27818  mdexchi  27820  atssma  27863  atoml2i  27868  chirredlem3  27877  mdsymlem1  27888  mdsymlem3  27890  dmdbr6ati  27908  dmdbr7ati  27909  cdjreui  27917  cdj3lem2b  27922  addltmulALT  27931  ssrmo  27962  difuncomp  28002  iundifdif  28014  imadifxp  28048  fresf1o  28068  fimacnvinrn2  28073  sspreima  28083  acunirnmpt  28098  acunirnmpt2  28099  aciunf1lem  28101  aciunf1  28102  disjdsct  28120  1stpreimas  28123  resf1o  28155  xrge0addge  28175  xlt2addrd  28176  xrge0infss  28178  f1ocnt  28209  ressmulgnn0  28280  xrge0neqmnf  28287  xrge0nre  28288  gsummpt2co  28378  gsummpt2d  28379  kerunit  28422  pmtrprfv2  28447  psgnfzto1stlem  28449  fzto1st  28452  psgnfzto1st  28454  submat1n  28467  submatres  28468  lmat22lem  28479  locfinreflem  28503  ldlfcntref  28517  pstmfval  28535  mndpluscn  28568  rge0scvg  28591  pnfneige0  28593  pl1cn  28597  nexple  28667  indval2  28672  gsumesum  28716  esumcst  28720  esumrnmpt2  28725  esumcvgsum  28745  esumgect  28747  esumcvgre  28748  esum2d  28750  esumiun  28751  pwsiga  28788  insiga  28795  elsigagen2  28806  inelpisys  28812  sigapisys  28813  unelldsys  28816  ldsysgenld  28818  measxun2  28868  volmeas  28890  ddemeas  28895  aean  28903  mbfmfun  28912  mbfmbfm  28916  1stmbfm  28918  2ndmbfm  28919  omsfval  28952  oms0  28955  omssubadd  28958  carsgclctunlem1  28975  sibfof  28998  eulerpartlemt  29027  eulerpartlemmf  29031  eulerpartlemgs2  29036  probun  29075  dstfrvclim1  29133  coinfliprv  29138  ballotlem2  29144  ballotlemfp1  29147  ballotlemic  29162  ballotlem1c  29163  plymulx0  29221  signsvtn0  29244  signstres  29249  bnj529  29336  bnj927  29365  bnj1379  29427  bnj1424  29435  bnj1436  29436  bnj1476  29443  bnj607  29512  bnj908  29527  bnj1097  29575  bnj1118  29578  bnj1128  29584  bnj1145  29587  bnj1154  29593  bnj1174  29597  bnj1189  29603  bnj1204  29606  bnj1388  29627  bnj1417  29635  cvmliftlem10  29802  mrsub0  29939  mrsubccat  29941  mrsubcn  29942  ghomgrpilem2  30089  bcprod  30158  bccolsum  30159  faclim  30166  dfon2lem3  30215  dfon2lem7  30219  dfon2lem8  30220  rdgprc0  30224  frrlem4  30301  frrlem5  30302  fvsingle  30469  unisnif  30474  funpartlem  30491  hfun  30727  trer  30754  clsun  30766  opnregcld  30768  cldregopn  30769  fnessref  30795  df3nandALT1  30839  lukshef-ax2  30857  nandsym1  30864  sylancl2  30944  bj-gl4  30960  bj-babygodel  30967  bj-babylob  30968  bj-alrimhi  30989  bj-nfext  31043  bj-ax9  31245  bj-snsetex  31303  bj-1upln0  31349  bj-inftyexpidisj  31394  bj-elccinfty  31398  finixpnum  31634  fin2so  31636  poimirlem9  31653  poimirlem13  31657  poimirlem14  31658  poimirlem25  31669  poimirlem26  31670  mblfinlem2  31682  mblfinlem3  31683  mblfinlem4  31684  ismblfin  31685  mbfresfi  31691  ftc1cnnc  31720  ftc1anclem6  31726  dvasin  31732  fnopabco  31753  frinfm  31766  nninfnub  31784  caushft  31794  bndss  31822  ispridl2  31975  notornotel1  32035  tsbi2  32080  abeq12  32103  rabeq12f  32104  axc11n-16  32218  lkr0f  32369  glbconN  32651  paddssat  33088  pclunN  33172  2polssN  33189  paddunN  33201  poldmj1N  33202  ltrnnid  33410  dibglbN  34443  istopclsd  35251  pellex  35389  monotoddzzfi  35500  jm2.23  35561  expdioph  35588  dford3lem1  35591  wopprc  35595  kelac1  35631  dfac21  35634  lsmfgcl  35642  pwssplit4  35657  isnumbasgrp  35676  dgraalem  35714  ifpbi1  35824  rp-fakeanorass  35860  rp-isfinite5  35865  superficl  35874  ssuncl  35877  sssymdifcl  35879  cnvtrrel  35905  brfvrcld2  35927  relexpxpmin  35952  relexpaddss  35953  brtrclfv2  35962  unhe1  36022  frege55lem1b  36132  frege58bid  36139  frege92  36192  imadisjlnd  36240  bcc0  36330  pm10.12  36348  pm11.61  36384  sbiota1  36426  bi1imp  36478  bi2imp  36479  bi3impb  36480  bi3impa  36481  bi13impib  36483  bi123impib  36484  bi13impia  36485  bi123impia  36486  bi13imp23  36489  bi13imp2  36490  bi12imp3  36491  dfvd1imp  36587  dfvd2imp  36624  e1bi  36650  e2bi  36653  e3bi  36769  3ornot23VD  36887  3impexpbicomVD  36897  3impexpbicomiVD  36898  tratrbVD  36902  ssralv2VD  36907  equncomiVD  36910  truniALTVD  36919  ee33VD  36920  csbingVD  36925  onfrALTlem3VD  36928  onfrALTlem2VD  36930  onfrALTlem1VD  36931  onfrALTVD  36932  csbsngVD  36934  csbxpgVD  36935  csbrngVD  36937  csbunigVD  36939  csbfv12gALTVD  36940  relopabVD  36942  2uasbanhVD  36952  vk15.4jVD  36955  unisnALT  36967  chordthmALT  36974  iunconlem2  36976  fnchoice  36994  elunnel2  37004  pwssfi  37025  uzwo4  37037  inabs3  37041  suprnmpt  37065  wessf1ornlem  37086  disjrnmpt2  37090  founiiun0  37092  disjf1o  37093  fompt  37094  disjinfi  37095  fzisoeu  37131  upbdrech  37136  ssfiunibd  37140  iuneqfzuzlem  37170  iuneqfzuz  37171  eliocre  37198  lbioc  37203  fsumiunss  37233  fmuldfeq  37237  infrglbOLD  37245  mccl  37254  climsuselem1  37262  climsuse  37263  ellimcabssub0  37273  islptre  37275  lptioo2  37287  lptioo1  37288  islpcn  37295  icccncfext  37341  cncfiooicclem1  37347  cncfiooicc  37348  cncfioobdlem  37350  dvbdfbdioo  37378  ioodvbdlimc1lem2  37380  ioodvbdlimc2lem  37382  dvnprodlem1  37394  dvnprodlem2  37395  dvnprodlem3  37396  volioc  37422  itgioocnicc  37427  stoweidlem28  37461  stoweidlem52  37486  stoweidlem57  37491  wallispilem3  37502  wallispilem4  37503  wallispi  37505  wallispi2lem1  37506  wallispi2lem2  37507  wallispi2  37508  stirlinglem7  37515  stirlinglem10  37518  stirlinglem12  37520  fourierdlem12  37554  fourierdlem20  37562  fourierdlem25  37567  fourierdlem33  37575  fourierdlem42  37584  fourierdlem48  37590  fourierdlem50  37592  fourierdlem52  37594  fourierdlem57  37599  fourierdlem58  37600  fourierdlem59  37601  fourierdlem65  37607  fourierdlem68  37610  fourierdlem70  37612  fourierdlem71  37613  fourierdlem73  37615  fourierdlem74  37616  fourierdlem75  37617  fourierdlem76  37618  fourierdlem80  37622  fourierdlem93  37635  fourierdlem101  37643  fourierdlem103  37645  fourierdlem104  37646  fourierswlem  37666  fouriersw  37667  etransclem26  37696  etransclem37  37707  saluncl  37729  salgenval  37733  intsaluni  37739  intsal  37740  salgencl  37741  sge00  37756  sge0sn  37759  sge0cl  37761  sge0f1o  37762  sge0less  37772  sge0rnbnd  37773  sge0pnffigt  37776  sge0lefi  37778  sge0ltfirp  37780  sge0resplit  37786  sge0split  37789  sge0iunmptlemfi  37793  sge0iunmptlemre  37795  sge0fodjrnlem  37796  sge0iunmpt  37798  iundjiun  37811  meadjun  37813  meassle  37814  meadjiunlem  37816  ismeannd  37818  meaiunlelem  37819  psmeasure  37822  carageneld  37836  caragenunidm  37842  omeunle  37850  omeiunltfirp  37853  caratheodorylem1  37860  caratheodory  37862  aifftbifffaibif  37913  aifftbifffaibifff  37914  abciffcbatnabciffncba  37921  abciffcbatnabciffncbai  37922  nabctnabc  37923  confun4  37934  confun5  37935  plcofph  37936  pldofph  37937  plvcofph  37938  plvcofphax  37939  plvofpos  37940  dandysum2p2e4  37990  2reu4a  38014  ndmaovrcl  38109  iccpartiun  38151  iccpartdisj  38154  dfodd5  38192  stgoldbwt  38280  nnsum3primesle9  38292  nnsum4primesodd  38294  nnsum4primesoddALTV  38295  nnsum4primeseven  38298  pfxccat3  38370  pfxccatpfx1  38371  elpwdifsn  38386  pr1eqbg  38387  usgra2pthlem1  38436  usgra2pth  38437  usgvincvad  38487  usgvincvadALT  38490  usg2edgneu  38495  usgedgvadf1lem2  38497  usgedgvadf1  38498  usgedgvadf1ALTlem2  38500  usgedgvadf1ALT  38501  usgo0s0  38518  usgo0s0ALT  38519  usgo1s0ALT  38520  usgrafisbaseALT  38523  usgrafisbaseALT2  38524  usgo1s0  38525  usgfis  38529  usgfisALT  38533  lmod0rng  38639  lidldomnnring  38701  fdmdifeqresdif  38896  altgsumbcALT  38907  ply1sclrmsm  38948  lcoop  38977  lincfsuppcl  38979  linccl  38980  lincvalsng  38982  lincvalpr  38984  lincvalsc0  38987  linc0scn0  38989  lincdifsn  38990  linc1  38991  lincsum  38995  lincscm  38996  lindslinindsimp2lem5  39028  snlindsntor  39037  lincresunit3lem2  39046  ldepsnlinclem1  39071  ldepsnlinclem2  39072  difmodm1lt  39099  nn0sumshdiglemB  39205
  Copyright terms: Public domain W3C validator