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

Theorem biimpi 194
Description: Infer an implication from a logical equivalence. (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 bi1 186 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
31, 2ax-mp 5 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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
This theorem is referenced by:  sylbi  195  sylib  196  sylbb  197  biimpri  206  mpbi  208  syl5bi  217  syl6ib  226  syl7bi  230  syl8ib  231  pm2.53  371  simplbi  458  simprbi  462  sylanb  470  sylan2b  473  pm3.1  496  orbi2i  517  pm2.32  524  anc2l  553  pm3.37  577  dfbi  627  pm2.76  846  pm5.15  887  pm5.16  888  pm5.75  935  rnlemOLD  963  simp1bi  1009  simp2bi  1010  simp3bi  1011  syl3an1b  1262  syl3an2b  1263  syl3an3b  1264  nic-ax  1510  19.25  1696  stdpc5v  1737  sbbii  1751  spvw  1761  excomim  1855  stdpc5  1913  sb9i  2172  axc11n-16  2270  exmoeu  2318  2mo  2370  2moOLD  2371  eqeq1d  2456  eqeq1OLD  2459  eleq2OLD  2529  gencbvex  3150  moeq  3272  euind  3283  reuind  3300  eqsbc3r  3381  ra4v  3409  ra4  3411  ssel  3483  unssd  3666  ssind  3708  n0moeu  3797  ss0  3815  uneqdifeq  3904  rabsnif  4085  prprc  4128  ssunsn2  4175  eqsn  4177  unisn2  4573  snexALT  4623  reusv3i  4644  snex  4678  brrelex12  5026  elrel  5093  exopxfr2  5136  dmxp  5210  xpssres  5296  elres  5297  elimasni  5352  xpdifid  5420  dmsnsnsn  5469  coi2  5507  xpco  5530  iotabi  5543  uniabio  5544  iotaint  5547  nfunv  5601  funun  5612  funcnv3  5631  funimass1  5643  funssxp  5726  f0dom0  5751  f1o00  5830  dffv3  5844  dffv2  5921  fndmin  5970  iinpreima  5993  fveqressseq  6003  fsn2  6047  ftpg  6057  f12dfv  6154  f13dfv  6155  nvocnv  6162  isoselem  6212  riotaxfrd  6262  oprabid  6297  mpt2difsnif  6368  ovima0  6427  sorpsscmpl  6564  unexg  6574  ordsson  6598  peano2  6693  1stval  6775  2ndval  6776  1stdm  6820  oprabco  6857  f1o2ndf1  6881  poxp  6885  suppval1  6897  funsssuppss  6918  fnsuppeq0  6920  imacosupp  6932  tz7.49c  7103  undifixp  7498  bren2  7539  ensym  7557  en1uniel  7580  domunsn  7660  limenpsi  7685  php4  7697  snnen2o  7699  isinf  7726  en2  7748  findcard2  7752  unfilem1  7776  suppssfifsupp  7836  fsuppunbi  7842  elfiun  7882  marypha1lem  7885  marypha2lem3  7889  supval2  7906  supmaxlemOLD  7916  brwdom2  7991  brwdom3  8000  sucprcreg  8017  preleq  8025  tcmin  8163  prwf  8220  r1pw  8254  rankuni2b  8262  rankr1id  8271  cardval3  8324  ficardom  8333  cardmin2  8370  isinfcard  8464  iscard3  8465  alephval3  8482  dfac9  8507  kmlem6  8526  ackbij1lem12  8602  fin23lem29  8712  fin23lem30  8713  fin23lem41  8723  isf32lem11  8734  isfin1-3  8757  fin1a2lem11  8781  fin1a2lem12  8782  fin1a2lem13  8783  axcc2lem  8807  dominf  8816  axdc4lem  8826  dominfac  8939  pwcfsdom  8949  cfpwsdom  8950  tskuni  9150  wfgru  9183  rpregt0  11234  supxrun  11510  elfz1end  11718  1fv  11796  elfzonlteqm1  11872  fzennn  12060  cardfz  12062  fsuppmapnn0fiubex  12080  fsuppmapnn0fiub0  12081  ser0  12141  crreczi  12273  faclbnd  12350  bcn1  12373  hashrabsn01  12424  hashge0  12438  hashssdif  12459  hashsnlei  12462  hashpw  12478  hash2prd  12502  ccatw2s1p1  12629  swrd0len0  12652  swrdtrcfv  12657  swrdswrd  12676  swrdccatwrd  12684  swrdccatin2  12703  swrdccat3  12708  swrdccat3a  12710  repsundef  12734  cshwlen  12761  s4f1o  12857  trclublem  12913  reltrclfv  12935  dmtrclfv  12936  relexpsucnnr  12942  sqrt0  13157  cau3lem  13269  harmonic  13752  mertenslem2  13776  prodf1  13782  fprodfac  13859  rpnnen2  14043  prmind2  14312  pceq0  14478  prmreclem6  14523  0ram  14622  ram0  14624  cshwsdisj  14667  cshwsiun  14668  ressbas2  14774  ressinbas  14779  ressval3d  14780  mrcuni  15110  mreexexlem4d  15136  catpropd  15197  initoid  15483  termoid  15484  initoeu2lem0  15491  arwhoma  15523  joinfval  15830  meetfval  15844  clatlem  15940  lubun  15952  psssdm  16045  ismgmn0  16073  plusfeq  16078  isnsgrp  16114  isnmnd  16123  grpissubg  16420  idrespermg  16635  symgextfv  16642  fvcosymgeq  16653  pmtrprfv3  16678  pmtr3ncomlem1  16697  psgnunilem4  16721  gsummptfzsplitl  17151  gsumzoppg  17165  gsum2dlem1  17193  gsum2dlem2  17194  gsum2d  17195  gsum2dOLD  17196  srg1zr  17375  staffn  17693  scafeq  17727  lbsexg  18005  lidldvgen  18098  ply1bascl2  18438  cply1mul  18530  lply1binom  18543  prmirred  18707  zlmassa  18736  frgpcyg  18785  ipfeq  18858  dsmmbas2  18941  frlmbas3  18978  mamufacex  19058  matsubgcell  19103  matinvgcell  19104  matvscacell  19105  mpt2matmul  19115  matepmcl  19131  matepm2cl  19132  mat1dimbas  19141  scmatscm  19182  smatvscl  19193  marrepcl  19233  marepvcl  19238  mulmarep1el  19241  mulmarep1gsum1  19242  mulmarep1gsum2  19243  submabas  19247  nfimdetndef  19258  mdetfval1  19259  m1detdiag  19266  mdetdiag  19268  mdetunilem7  19287  mdetunilem9  19289  m2detleib  19300  gsummatr01lem3  19326  smadiadetlem4  19338  slesolinv  19349  slesolinvbi  19350  slesolex  19351  cramerimplem2  19353  pmatcoe1fsupp  19369  mat2pmatbas  19394  mat2pmatmul  19399  mat2pmatlin  19403  m2cpminvid2lem  19422  decpmatmul  19440  monmatcollpw  19447  pmatcollpw3fi  19453  pm2mpf1  19467  pm2mpghm  19484  fvmptnn04ifb  19519  cayhamlem1  19534  isbasis3g  19617  isopn2  19700  ntrval2  19719  toponmre  19761  innei  19793  restcld  19840  restcldi  19841  neitr  19848  discmp  20065  cmpsublem  20066  cmpsub  20067  2ndcctbss  20122  ssref  20179  lfinun  20192  dissnref  20195  ptcnp  20289  imasnopn  20357  imasncld  20358  imasncls  20359  kqf  20414  fbun  20507  opnfbas  20509  supfil  20562  ufprim  20576  acufl  20584  filufint  20587  ufldom  20629  hausflf2  20665  alexsubALTlem4  20716  cnextfval  20728  cnextfun  20730  cnextfres  20734  trust  20898  utoptop  20903  ustuqtop1  20910  metustidOLD  21228  metustid  21229  metustfbasOLD  21234  metustfbas  21235  cfilucfilOLD  21238  cfilucfil  21239  metustblOLD  21249  metustbl  21250  restmetu  21256  zlmclm  21761  cphassr  21824  ovolun  22076  volun  22121  vitalilem2  22184  dvmptfsum  22542  rolle  22557  ulmcaulem  22955  logfac  23154  logno1  23185  logreclem  23301  cxplogb  23325  leibpilem1  23468  prmorcht  23650  pclogsum  23688  2sqlem10  23847  chto1lb  23861  tgldimor  24094  axcontlem7  24475  usgraop  24552  ausisusgra  24557  usgra2edg1  24585  usgrarnedg  24586  usgraedg4  24589  usgra1v  24592  usgraidx2vlem2  24594  usgraidx2v  24595  usgrares1  24612  nbgrassvwo  24639  nbgrassvwo2  24640  nb3graprlem2  24654  nb3grapr  24655  nb3grapr2  24656  nb3gra2nb  24657  cusgra3v  24666  cusgrafilem2  24682  usgrasscusgra  24685  uvtxnbgra  24695  uvtxnb  24699  2trllemH  24756  2trllemE  24757  constr1trl  24792  usgra2adedgwlkonALT  24818  usgra2wlkspthlem2  24822  fargshiftfo  24840  wwlknndef  24939  wwlkextproplem3  24945  clwlkswlks  24960  clwwlknndef  24975  clwlkisclwwlklem2a4  24986  clwlkisclwwlklem1  24989  clwwlkf  24996  clwwlkvbij  25003  wwlkext2clwwlk  25005  clwwnisshclwwn  25011  erclwwlkref  25015  erclwwlknref  25027  erclwwlknsym  25028  erclwwlkntr  25029  hashecclwwlkn1  25036  usghashecclwwlk  25037  clwlkfoclwwlk  25047  el2wlkonot  25071  el2spthonot  25072  el2wlkonotot0  25074  vdgrnn0pnf  25111  clwlknclwlkdifs  25162  eupatrl  25170  frgra3v  25204  3vfriswmgra  25207  1to3vfriswmgra  25209  1to3vfriendship  25210  2pthfrgra  25213  4cycl2v2nb  25218  n4cyclfrgra  25220  frgranbnb  25222  frgrancvvdeqlem4  25235  frgrawopreg  25251  frg2woteqm  25261  usg2spot2nb  25267  numclwwlkovf2ex  25288  numclwwlk3lem  25310  grpoidinvlem3  25406  nmlno0lem  25906  blocni  25918  pythi  25963  normpythi  26257  shmodsi  26505  omlsilem  26518  pjchi  26548  chlubii  26588  osumi  26758  nmlnop0iALT  27112  cnlnssadj  27197  nmopcoi  27212  mdbr3  27414  mdbr4  27415  ssmd1  27428  dmdsl3  27432  mdslmd1lem2  27443  mdslmd4i  27450  mdexchi  27452  atssma  27495  atoml2i  27500  chirredlem3  27509  mdsymlem1  27520  mdsymlem3  27522  dmdbr6ati  27540  dmdbr7ati  27541  cdjreui  27549  cdj3lem2b  27554  addltmulALT  27563  ssrmo  27591  iundifdif  27640  imadifxp  27672  fresf1o  27692  fimacnvinrn2  27697  sspreima  27706  acunirnmpt  27726  acunirnmpt2  27727  aciunf1lem  27729  aciunf1  27730  disjdsct  27749  1stpreimas  27752  resf1o  27784  xlt2addrd  27809  xrge0infss  27811  ressmulgnn0  27906  xrge0neqmnf  27913  xrge0nre  27914  gsummpt2co  28005  gsummpt2d  28006  kerunit  28048  locfinreflem  28078  ldlfcntref  28092  pstmfval  28110  mndpluscn  28143  rge0scvg  28166  pnfneige0  28168  pl1cn  28172  nexple  28239  indval2  28244  gsumesum  28288  esumcst  28292  esumrnmpt2  28297  esumcvgsum  28317  esumgect  28319  esumcvgre  28320  esum2d  28322  esumiun  28323  pwsiga  28360  insiga  28367  elsigagen2  28378  sigapisys  28384  measxun2  28418  volmeas  28440  ddemeas  28445  aean  28453  mbfmfun  28462  mbfmbfm  28466  1stmbfm  28468  2ndmbfm  28469  omsfval  28502  oms0  28505  omssubadd  28508  carsgclctunlem1  28525  sibfof  28546  eulerpartlemt  28574  eulerpartlemmf  28578  eulerpartlemgs2  28583  probun  28622  dstfrvclim1  28680  coinfliprv  28685  ballotlem2  28691  ballotlemfp1  28694  ballotlemic  28709  ballotlem1c  28710  plymulx0  28768  signsvtn0  28791  signstres  28796  cvmliftlem10  29003  mrsub0  29140  mrsubccat  29142  mrsubcn  29143  ghomgrpilem2  29290  risefacp1  29392  fallfacp1  29393  faclim  29412  dfon2lem3  29457  dfon2lem7  29461  dfon2lem8  29462  rdgprc0  29466  wfrlem4  29586  wfrlem5  29587  wfrlem10  29592  wfrlem15  29597  frrlem4  29630  frrlem5  29631  fvsingle  29798  unisnif  29803  funpartlem  29820  hfun  30063  df3nandALT1  30090  lukshef-ax2  30108  nandsym1  30115  finixpnum  30278  fin2so  30280  mblfinlem2  30292  mblfinlem3  30293  mblfinlem4  30294  ismblfin  30295  mbfresfi  30301  ftc1cnnc  30329  ftc1anclem6  30335  dvasin  30343  trer  30374  clsun  30386  opnregcld  30388  cldregopn  30389  fnessref  30415  fnopabco  30453  frinfm  30466  nninfnub  30484  caushft  30494  bndss  30522  ispridl2  30675  notornotel1  30735  tsbi2  30781  abeq12  30804  rabeq12f  30805  istopclsd  30872  pellex  31010  monotoddzzfi  31117  jm2.23  31177  expdioph  31204  dford3lem1  31207  wopprc  31211  inisegn0  31228  kelac1  31248  dfac21  31251  lsmfgcl  31259  pwssplit4  31274  isnumbasgrp  31297  dgraalem  31335  lcmcllem  31443  bcc0  31486  pm10.12  31504  pm11.61  31540  sbiota1  31582  fnchoice  31644  elunnel1  31654  elunnel2  31655  suprnmpt  31691  fzisoeu  31739  upbdrech  31744  ssfiunibd  31748  elicore  31776  eliocre  31786  lbioc  31792  fmuldfeq  31816  infrglb  31823  fprodle  31843  mccl  31845  climsuselem1  31852  climsuse  31853  ellimcabssub0  31862  islptre  31864  lptioo2  31876  lptioo1  31877  islpcn  31884  icccncfext  31929  cncfiooicclem1  31935  cncfiooicc  31936  cncfioobdlem  31938  dvbdfbdioo  31966  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  dvnprodlem1  31982  dvnprodlem2  31983  dvnprodlem3  31984  volioc  32010  itgioocnicc  32015  stoweidlem28  32049  stoweidlem52  32073  stoweidlem57  32078  wallispilem3  32088  wallispilem4  32089  wallispi  32091  wallispi2lem1  32092  wallispi2lem2  32093  wallispi2  32094  stirlinglem7  32101  stirlinglem10  32104  stirlinglem12  32106  fourierdlem12  32140  fourierdlem20  32148  fourierdlem25  32153  fourierdlem33  32161  fourierdlem42  32170  fourierdlem48  32176  fourierdlem50  32178  fourierdlem52  32180  fourierdlem57  32185  fourierdlem58  32186  fourierdlem59  32187  fourierdlem65  32193  fourierdlem68  32196  fourierdlem70  32198  fourierdlem71  32199  fourierdlem73  32201  fourierdlem74  32202  fourierdlem75  32203  fourierdlem76  32204  fourierdlem80  32208  fourierdlem93  32221  fourierdlem101  32229  fourierdlem103  32231  fourierdlem104  32232  fourierswlem  32252  fouriersw  32253  etransclem26  32282  etransclem37  32293  dandysum2p2e4  32409  2reu4a  32433  ndmaovrcl  32528  dfodd5  32571  pfxccat3  32654  pfxccatpfx1  32655  elpwdifsn  32670  pr1eqbg  32671  el2fzo  32713  usgra2pthlem1  32725  usgra2pth  32726  usgvincvad  32776  usgvincvadALT  32779  usg2edgneu  32784  usgedgvadf1lem2  32786  usgedgvadf1  32787  usgedgvadf1ALTlem2  32789  usgedgvadf1ALT  32790  usgo0s0  32807  usgo0s0ALT  32808  usgo1s0ALT  32809  usgrafisbaseALT  32812  usgrafisbaseALT2  32813  usgo1s0  32814  usgfis  32818  usgfisALT  32822  lmod0rng  32928  lidldomnnring  32990  fdmdifeqresdif  33185  altgsumbcALT  33196  ply1sclrmsm  33237  lcoop  33266  lincfsuppcl  33268  linccl  33269  lincvalsng  33271  lincvalpr  33273  lincvalsc0  33276  linc0scn0  33278  lincdifsn  33279  linc1  33280  lincsum  33284  lincscm  33285  lindslinindsimp2lem5  33317  snlindsntor  33326  lincresunit3lem2  33335  ldepsnlinclem1  33360  ldepsnlinclem2  33361  difmodm1lt  33389  nn0sumshdiglemB  33495  biimp  33637  bi2imp  33638  bi3impb  33639  bi3impa  33640  bi13impib  33642  bi123impib  33643  bi13impia  33644  bi123impia  33645  bi13imp23  33648  bi13imp2  33649  bi12imp3  33650  dfvd1imp  33746  dfvd2imp  33783  e1bi  33809  e2bi  33812  e3bi  33929  3ornot23VD  34047  3impexpbicomVD  34057  3impexpbicomiVD  34058  tratrbVD  34062  ssralv2VD  34067  equncomiVD  34070  truniALTVD  34079  ee33VD  34080  csbingVD  34085  onfrALTlem3VD  34088  onfrALTlem2VD  34090  onfrALTlem1VD  34091  onfrALTVD  34092  csbsngVD  34094  csbxpgVD  34095  csbrngVD  34097  csbunigVD  34099  csbfv12gALTVD  34100  relopabVD  34102  2uasbanhVD  34112  vk15.4jVD  34115  unisnALT  34127  chordthmALT  34134  iunconlem2  34136  bnj529  34199  bnj927  34228  bnj1379  34290  bnj1424  34298  bnj1436  34299  bnj1476  34306  bnj607  34375  bnj908  34390  bnj1097  34438  bnj1118  34441  bnj1128  34447  bnj1145  34450  bnj1154  34456  bnj1174  34460  bnj1189  34466  bnj1204  34469  bnj1388  34490  bnj1417  34498  sylancl2  34569  bj-gl4  34585  bj-babygodel  34592  bj-babylob  34593  bj-alrimhi  34614  bj-nfext  34667  bj-ax9  34865  bj-snsetex  34922  bj-1upln0  34968  bj-inftyexpidisj  35013  bj-elccinfty  35017  lkr0f  35216  glbconN  35498  paddssat  35935  pclunN  36019  2polssN  36036  paddunN  36048  poldmj1N  36049  ltrnnid  36257  dibglbN  37290  ifpbi1  38096  rp-fakeanorass  38151  rp-isfinite5  38156  superficl  38165  ssuncl  38168  sssymdifcl  38170  cnvtrrel  38189  relexpaddss  38205  relexpxpmin  38226  unhe1  38258  frege55lem1b  38372  frege58bid  38379  imadisjlnd  38425
  Copyright terms: Public domain W3C validator