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

Theorem biimpi 186
Description: Infer an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)
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 178 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
31, 2ax-mp 8 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  sylbi  187  sylib  188  biimpri  197  mpbi  199  syl5bi  208  syl6ib  217  syl7bi  221  syl8ib  222  bitri  240  pm2.53  362  simplbi  446  simprbi  450  sylanb  458  sylan2b  461  pm3.1  484  orbi2i  505  pm2.32  512  anc2l  538  pm3.37  562  dfbi  610  pm2.76  821  pm5.15  859  pm5.16  860  pm5.75  903  rnlem  931  simp1bi  970  simp2bi  971  simp3bi  972  syl3an1b  1218  syl3an2b  1219  syl3an3b  1220  nic-ax  1428  19.25  1590  sbbii  1634  hbn1fw  1679  ax10-16  2129  exmoeu  2185  2mo  2221  eqeq1  2289  eleq2  2344  gencbvex  2830  moeq  2941  euind  2952  reuind  2968  eqsbc3r  3048  ssel  3174  unssd  3351  ssind  3393  n0moeu  3467  ss0  3485  uneqdifeq  3542  prprc  3738  ssunsn2  3773  eqsn  3775  trint  4128  snexALT  4196  snex  4216  pocl  4321  wefrc  4387  unexg  4521  unisn2  4522  reusv3i  4541  ordsson  4581  peano2  4676  brrelex12  4726  elrel  4789  dmxp  4897  xpssres  4989  elres  4990  elimasni  5040  dmsnsnsn  5151  coi2  5189  iotabi  5228  uniabio  5229  iotaint  5232  nfunv  5285  funun  5296  funcnv3  5311  funimass1  5325  funssxp  5402  f1o00  5508  dffv3  5521  dffv2  5592  fndmin  5632  iinpreima  5655  fsn2  5698  fnsuppeq0  5733  isoselem  5838  oprabid  5882  1stval  6124  2ndval  6125  1stdm  6167  exopxfr2  6184  oprabco  6203  poxp  6227  sorpsscmpl  6288  riotaxfrd  6336  tz7.49c  6458  undifixp  6852  bren2  6892  ensym  6910  domunsn  7011  limenpsi  7036  php4  7048  isinf  7076  en2  7094  findcard2  7098  unfilem1  7121  fissuni  7160  elfiun  7183  marypha1lem  7186  marypha2lem3  7190  supmaxlem  7215  brwdom2  7287  brwdom3  7296  preleq  7318  inf3lem2  7330  tcmin  7426  rankvalb  7469  prwf  7483  r1pw  7517  rankuni2b  7525  rankr1id  7534  cardval3  7585  ficardom  7594  cardmin2  7631  isinfcard  7719  iscard3  7720  alephval3  7737  dfac9  7762  kmlem6  7781  ackbij1lem12  7857  fin23lem29  7967  fin23lem30  7968  fin23lem41  7978  isf32lem11  7989  isfin1-3  8012  fin1a2lem11  8036  fin1a2lem12  8037  fin1a2lem13  8038  axcc2lem  8062  dominf  8071  axdc4lem  8081  dominfac  8195  pwcfsdom  8205  cfpwsdom  8206  tskuni  8405  wfgru  8438  rpregt0  10367  xrrebnd  10497  xaddf  10551  supxrun  10634  elfz1end  10820  fzennn  11030  cardfz  11032  ser0  11098  crreczi  11226  faclbnd  11303  bcn1  11325  hashssdif  11374  hashsnlei  11376  hashpw  11388  hashfun  11389  sqr0  11727  cau3lem  11838  harmonic  12317  mertenslem2  12341  rpnnen2  12504  prmind2  12769  pceq0  12923  prmreclem6  12968  0ram  13067  ram0  13069  ressbas2  13199  ressinbas  13204  mrcuni  13523  mreexexlem4d  13549  catpropd  13612  arwhoma  13877  lubun  14227  psssdm  14325  plusfeq  14381  gsum2d  15223  staffn  15614  scafeq  15647  lbsexg  15917  lidldvgen  16007  ply1bascl2  16285  prmirred  16448  zlmassa  16478  frgpcyg  16527  ipfeq  16554  isbasis3g  16687  isopn2  16769  ntrval2  16788  toponmre  16830  innei  16862  restcld  16903  restcldi  16904  discmp  17125  cmpsublem  17126  cmpsub  17127  2ndcctbss  17181  ptcnp  17316  kqf  17438  fbun  17535  opnfbas  17537  cfinfil  17588  supfil  17590  ufprim  17604  acufl  17612  filufint  17615  ufldom  17657  hausflf2  17693  alexsubALTlem4  17744  zlmclm  18593  cphassr  18647  ovolun  18858  volun  18902  dyadmax  18953  vitalilem2  18964  dvmptfsum  19322  rolle  19337  ulmcaulem  19771  logfac  19954  logno1  19983  logreclem  20116  leibpilem1  20236  prmorcht  20416  pclogsum  20454  2sqlem10  20613  chto1lb  20627  grpoidinvlem3  20873  nmlno0lem  21371  blocni  21383  pythi  21428  normpythi  21721  isch3  21821  shmodsi  21968  omlsilem  21981  pjchi  22011  chlubii  22051  osumi  22221  nmlnop0iALT  22575  nmopun  22594  cnlnssadj  22660  nmopcoi  22675  mdbr3  22877  mdbr4  22878  ssmd1  22891  dmdsl3  22895  mdslmd1lem2  22906  mdslmd4i  22913  mdexchi  22915  atssma  22958  atoml2i  22963  chirredlem3  22972  mdsymlem1  22983  mdsymlem3  22985  dmdbr6ati  23003  dmdbr7ati  23004  cdjreui  23012  cdj3lem2b  23017  addltmulALT  23026  ballotlem2  23047  ballotlemfp1  23050  ballotlemic  23065  ballotlem1c  23066  ballotlemro  23081  ssrmo  23148  elim2ifim  23153  iundifdifd  23159  iundifdif  23160  fimacnvinrn2  23200  sspreima  23210  xlt2addrd  23253  mndpluscn  23299  ressmulgnn0  23309  xrge0iifhom  23319  xrge0neqmnf  23330  disjdsct  23369  rge0scvg  23373  pnfneige0  23374  hashge0  23386  logbcl  23399  esumnul  23427  esumcst  23436  esumsn  23437  esumpinfval  23441  pwsiga  23491  insiga  23498  elsigagen2  23509  measxun2  23538  measssd  23543  mbfmfun  23559  mbfmbfm  23563  1stmbfm  23565  2ndmbfm  23566  indval2  23598  probun  23622  totprobd  23629  dstfrvclim1  23678  coinfliprv  23683  cvmliftlem10  23825  ghomgrpilem2  23993  dfon2lem3  24141  dfon2lem7  24145  dfon2lem8  24146  rdgprc0  24150  wfrlem4  24259  wfrlem5  24260  wfrlem10  24265  wfrlem15  24270  frrlem4  24284  frrlem5  24285  unisnif  24464  axcontlem7  24598  hfun  24808  df3nandALT1  24835  lukshef-ax2  24854  nandsym1  24861  bibox  24982  binxt  24984  bidia  24989  splint  25048  twsymr  25078  imfstnrelc  25081  isfinite1b  25106  sssu  25141  prmapcp2  25157  supaub  25273  geme2  25275  toplat  25290  clfsebsr  25349  muldisc  25481  svli2  25484  intopcoaconb  25540  usptop  25550  limptlimpr2lem1  25574  limptlimpr2lem2  25575  islimrs  25580  flfneic  25624  supnufb  25630  dmrngcmp  25751  homib  25796  cmpmon  25815  idmon  25817  iepiclem  25823  idsubc  25851  idsubidsup  25857  idsubfun  25858  propsrc  25868  inttaror  25900  prismorcsetlemc  25917  domcatfun  25925  codcatfun  25934  idcatfun  25941  cmp2morpcats  25961  cmp2morpdom  25964  isconc2  26007  lineval4a  26087  isconcl6ab  26104  abhp  26173  trer  26227  clsun  26246  opnregcld  26248  cldregopn  26249  ssref  26283  fnessref  26293  fnopabco  26388  frinfm  26416  nninfnub  26461  caushft  26477  bndss  26510  ispridl2  26663  istopclsd  26775  pellex  26920  rmspecsqrnq  26991  monotoddzzfi  27027  jm2.23  27089  expdioph  27116  dford3lem1  27119  wopprc  27123  inisegn0  27140  kelac1  27161  dfac21  27164  lsmfgcl  27172  pwssplit4  27191  dsmmbas2  27203  isnumbasgrp  27272  dgraalem  27350  en1uniel  27380  psgnunilem4  27420  pm10.12  27553  pm11.61  27592  sbiota1  27634  fnchoice  27700  fmuldfeq  27713  infrglb  27722  climsuselem1  27733  climsuse  27734  stoweidlem16  27765  stoweidlem17  27766  stoweidlem20  27769  stoweidlem28  27777  stoweidlem31  27780  stoweidlem42  27791  stoweidlem48  27797  stoweidlem51  27800  stoweidlem52  27801  stoweidlem54  27803  stoweidlem57  27806  wallispilem3  27816  wallispilem4  27817  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  wallispi2  27822  stirlinglem7  27829  stirlinglem10  27832  stirlinglem12  27834  stirlinglem13  27835  aibandbiaiffaiffb  27862  aibandbiaiaiffb  27863  notatnand  27864  aistia  27865  aisfina  27866  bothfbothsame  27868  axorbtnotaiffb  27871  aiffnbandciffatnotciffb  27872  axorbciffatcxorb  27873  aibnbna  27874  aisbnaxb  27879  abnotbtaxb  27884  abnotataxb  27885  dandysum2p2e4  27943  2reu4a  27967  ndmaovrcl  28064  s4f1o  28093  usgra1v  28126  nbcusgra  28159  uvtxnbgra  28165  frgra3v  28180  3vfriswmgra  28183  1to3vfriswmgra  28185  1to3vfriendship  28186  dfvd1imp  28344  dfvd2imp  28375  e1bi  28401  e2bi  28404  e3bi  28513  3ornot23VD  28623  3impexpbicomVD  28633  3impexpbicomiVD  28634  tratrbVD  28637  ssralv2VD  28642  equncomiVD  28645  truniALTVD  28654  ee33VD  28655  csbingVD  28660  onfrALTlem3VD  28663  onfrALTlem2VD  28665  onfrALTlem1VD  28666  onfrALTVD  28667  csbsngVD  28669  csbxpgVD  28670  csbrngVD  28672  csbunigVD  28674  csbfv12gALTVD  28675  relopabVD  28677  2uasbanhVD  28687  vk15.4jVD  28690  unisnALT  28702  chordthmALT  28710  bnj529  28770  bnj927  28800  bnj1379  28863  bnj1424  28871  bnj1436  28872  bnj1476  28879  bnj607  28948  bnj849  28957  bnj908  28963  bnj1097  29011  bnj1118  29014  bnj1128  29020  bnj1145  29023  bnj1154  29029  bnj1174  29033  bnj1189  29039  bnj1204  29042  bnj1279  29048  bnj1388  29063  bnj1417  29071  ax12OLD  29105  lubunNEW  29163  lkr0f  29284  glbconN  29566  paddssat  30003  pclunN  30087  2polssN  30104  paddunN  30116  poldmj1N  30117  ltrnnid  30325  dibglbN  31356
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator