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

Theorem mpbi 200
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbi.min  |-  ph
mpbi.maj  |-  ( ph  <->  ps )
Assertion
Ref Expression
mpbi  |-  ps

Proof of Theorem mpbi
StepHypRef Expression
1 mpbi.min . 2  |-  ph
2 mpbi.maj . . 3  |-  ( ph  <->  ps )
32biimpi 187 . 2  |-  ( ph  ->  ps )
41, 3ax-mp 8 1  |-  ps
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  pm5.74i  237  notbii  288  pm5.19  350  ori  365  imori  403  pm4.71i  614  pm4.71ri  615  pm5.32i  619  pm3.24  853  pm5.16  861  biluk  900  4exmid  906  dn1  933  3ori  1244  trubifal  1360  nic-dfim  1443  nic-dfneg  1444  nic-mp  1445  nic-mpALT  1446  tbw-negdf  1473  rb-imdf  1524  mpto2  1543  mpto2OLD  1544  mtp-xorOLD  1546  mpgbi  1558  19.35i  1611  19.36i  1893  19.37aiv  1923  ax9  1953  sbie  2149  sbco  2158  sbidm  2160  axi12  2415  eqcomi  2440  eqtri  2456  eleqtri  2508  neii  2603  neeqtri  2622  nesymi  2641  necomi  2686  neli  2697  nrex  2808  rexlimi  2823  isseti  2962  vtocl2  3007  vtocl3  3008  eueq1  3107  euxfr2  3119  cdeqri  3147  sseqtri  3380  3sstr3i  3386  pssn2lp  3448  equncomi  3493  unssi  3522  ssini  3564  unabs  3571  inabs  3572  dfin4  3581  npss0  3666  difid  3696  disjdif  3700  difin0  3701  snid  3841  iinrab2  4154  rintn0  4181  breqtri  4235  axsep  4329  bm1.3ii  4333  ax9vsep  4334  zfnuleu  4335  notzfaus  4374  zfpow  4378  dtru  4390  dtruALT  4396  dtruALT2  4408  copsexg  4442  uniop  4459  pwundif  4490  onunisuci  4695  zfun  4702  reusv2lem4  4727  reuxfr2d  4746  op1stb  4758  tfinds2  4843  omon  4856  relop  5023  rn0  5127  dmresi  5196  issref  5247  somincom  5271  cnvcnv  5323  rescnvcnv  5332  cnvcnvres  5333  cnvsn  5352  cocnvcnv2  5381  cores2  5382  co01  5384  relcoi1  5398  cnviin  5409  iota4an  5437  fnopab  5569  mpt0  5572  fnmpti  5573  f1cnvcnv  5647  f1ovi  5714  fvco4i  5801  fmpti  5892  fvsnun2  5929  funiunfv  5995  oprabss  6159  relmptopab  6292  2nd0  6354  f1stres  6368  f2ndres  6369  relmpt2opab  6429  df1st2  6433  df2nd2  6434  fsplit  6451  reldmtpos  6487  dftpos4  6498  tpostpos  6499  tpos0  6509  smo0  6620  tfrlem14  6652  tfrlem16  6654  rdgsucg  6681  rdglimg  6683  frfnom  6692  oawordeulem  6797  uniixp  7085  dfdom2  7133  ssdomg  7153  xpcomf1o  7197  sbthlem5  7221  pwdom  7259  limensuci  7283  fiint  7383  fidomdm  7388  pwfilem  7401  mptfi  7406  fisn  7432  dffi3  7436  ordtypelem6  7492  ordtypelem7  7493  wemaplem2  7516  wdompwdom  7546  harwdom  7558  suc11reg  7574  zfinf  7594  axinf2  7595  noinfep  7614  cantnfvalf  7620  cantnflt  7627  cantnf0  7630  cantnf  7649  tz9.1c  7666  tc2  7681  r111  7701  r1tr2  7703  r1ordg  7704  r1sssuc  7709  r1val1  7712  tz9.13  7717  r1elssi  7731  pwwf  7733  rankopb  7778  rankeq0b  7786  ranksuc  7791  rankxplim  7803  rankxplim3  7805  rankxpsuc  7806  cp  7815  karden  7819  card0  7845  cardlim  7859  cardom  7873  infxpenlem  7895  alephsuc2  7961  alephgeom  7963  unialeph  7982  dfac4  8003  dfacacn  8021  cda1dif  8056  pm110.643  8057  infcda1  8073  ackbij1lem13  8112  ackbij2  8123  cf0  8131  cfsuc  8137  cfom  8144  cfslb2n  8148  ominf4  8192  fin23lem17  8218  fin23lem28  8220  fin23lem30  8222  fin23lem31  8223  fin23lem40  8231  isfin1-3  8266  dfacfin7  8279  fin1a2lem6  8285  itunitc1  8300  axcc3  8318  dcomex  8327  axdc2lem  8328  axcclem  8337  zfac  8340  ac3  8342  ackm  8345  axac2  8346  axac  8347  axaci  8348  cardeqv  8349  numth2  8351  numth  8352  brdom3  8406  fin71ac  8411  cardf  8425  aleph1  8446  cfpwsdom  8459  smobeth  8461  zfcndrep  8489  zfcndpow  8491  zfcndac  8494  gch2  8554  wunex3  8616  tskpr  8645  inar1  8650  rankcf  8652  tskcard  8656  tskuni  8658  grothpw  8701  axgroth4  8707  grothprim  8709  inaprc  8711  dmaddpi  8767  dmmulpi  8768  1lt2pi  8782  addpqf  8821  mulpqf  8823  1lt2nq  8850  supsrlem  8986  ssxr  9145  subf  9307  negne0i  9375  negdii  9384  mulnzcnopr  9668  lbinfm  9961  infmsup  9986  infmrgelb  9988  infmrlb  9989  halflt1  10189  nn0ssz  10302  zeo  10355  numlt  10401  numltc  10402  uzf  10491  uzinfmi  10555  xaddf  10810  xsubge0  10840  xmulf  10851  infmxrcl  10895  infmxrlb  10912  infmxrgelb  10913  xrinfm0  10915  ixxf  10926  ixxssxr  10928  iooval2  10949  ioof  11002  unirnioo  11004  dfioo2  11005  fzval2  11046  fzf  11047  fz10  11075  4fvwrd4  11121  fzof  11137  fzo0  11159  injresinjlem  11199  om2uzoi  11295  faclbnd4lem1  11584  hashkf  11620  hashgval  11621  hashinf  11623  hashnn0n0nn  11664  hashbclem  11701  wrdexg  11739  rev0  11796  f1oun2prg  11864  sqr2gt1lt2  12080  limsupgord  12266  limsupval  12268  fclim  12347  fsumrelem  12586  ackbijnn  12607  incexclem  12616  incexc  12617  arisum2  12640  georeclim  12649  geoisumr  12655  0.999...  12658  geoihalfsum  12659  ege2le3  12692  sin0  12750  ef01bndlem  12785  cos2bnd  12789  cos01gt0  12792  sincos2sgn  12795  sin4lt0  12796  rpnnen2lem3  12816  rpnnen2lem9  12822  rexpen  12827  cnso  12846  dvdslelem  12894  divalglem1  12914  divalglem5  12917  divalglem6  12918  divalglem10  12922  bitsfzolem  12946  bitsfzo  12947  0bits  12951  bitsinv1lem  12953  sadcf  12965  sadcadd  12970  bitsshft  12987  smupf  12990  gcdf  13019  eucalgf  13074  isprm3  13088  2prm  13095  dfphi2  13163  odzval  13177  pockthi  13275  prmreclem2  13285  prmrec  13290  vdwapf  13340  vdwap0  13344  vdwlem6  13354  ramval  13376  ramcl2lem  13377  karatsuba  13420  1259lem5  13454  2503lem3  13458  4001lem4  13463  structcnvcnv  13480  structfn  13482  strlemor1  13556  strleun  13559  prdsval  13678  prdsds  13686  imasdsfn  13740  imasdsval  13741  imasvscafn  13762  xpsc0  13785  xpsc1  13786  xpsff1o  13793  sscpwex  14015  wunfunc  14096  wunnat  14153  eldmcoa  14220  coapm  14226  catcfuccl  14264  catcxpccl  14304  yonedainv  14378  plusffval  14702  grpinvfvi  14846  mulgfvi  14894  odval  15172  odf  15175  gexval  15212  sylow3lem2  15262  oppglsm  15276  efgmf  15345  efgval  15349  efgsf  15361  0frgp  15411  gsumzaddlem  15526  dmdprd  15559  dprdval  15561  invrfval  15778  drngui  15841  scaffval  15968  lssintcl  16040  mplsubrglem  16502  opsrtoslem2  16545  cnfld0  16725  cnfld1  16726  cnfldsub  16729  xrsds  16741  ipffval  16879  ocv1  16906  eltpsi  17011  fctop  17068  cctop  17070  ppttop  17071  epttop  17073  leordtvallem1  17274  leordtvallem2  17275  iccordt  17278  iscnp2  17303  discmp  17461  concompcld  17497  1stcrestlem  17515  2ndcdisj  17519  topnlly  17554  disllycmp  17561  dis1stc  17562  txuni2  17597  xkotf  17617  dfac14lem  17649  prdstps  17661  txindis  17666  tx1stc  17682  xkohaus  17685  xkoptsub  17686  cnmpt1st  17700  cnmpt2nd  17701  ptcmpfi  17845  filcon  17915  trfil1  17918  fin1aufil  17964  tgpconcompeqg  18141  tgpconcomp  18142  tsmsres  18173  trust  18259  met1stc  18551  dscmet  18620  nmoval  18749  retopon  18797  cnfldtopon  18817  xrsxmet  18840  xrsmopn  18843  metdsval  18877  iimulcn  18963  icopnfhmeo  18968  iccpnfhmeo  18970  xrhmeo  18971  xrhmph  18972  cnheiborlem  18979  lebnumii  18991  ishtpy  18997  htpycc  19005  pco1  19040  pcohtpylem  19044  pcopt  19047  pcopt2  19048  pcoass  19049  pcorevlem  19051  cfilresi  19248  ovolval  19370  ovolf  19378  ovoliunlem3  19400  ovolicc1  19412  ovolicc2  19418  volf  19425  ioorf  19465  dyadf  19483  dyadmbl  19492  vitalilem4  19503  vitalilem5  19504  vitali  19505  mbfimaopnlem  19547  mbflimsup  19558  0plef  19564  i1fima  19570  i1fima2  19571  i1fd  19573  itg1ge0  19578  itg10  19580  i1f1lem  19581  i1fadd  19587  i1fmul  19588  i1fmulc  19595  mbfi1fseqlem5  19611  itg2addlem  19650  reldv  19757  dvbsss  19789  dvef  19864  dvlt0  19889  lhop1lem  19897  deg1fvi  20008  plypf1  20131  coeeulem  20143  coeeu  20144  vieta1lem2  20228  elqaalem1  20236  elqaalem3  20238  aannenlem3  20247  aalioulem2  20250  aalioulem3  20251  dvradcnv  20337  pserulm  20338  pserdvlem2  20344  abelthlem6  20352  sinhalfpilem  20374  sincos4thpi  20421  tan4thpi  20422  sincos6thpi  20423  pige3  20425  resinf1o  20438  tanord1  20439  tanregt0  20441  relogrn  20459  dfrelog  20463  logneg  20482  logltb  20494  logcn  20538  logf1o2  20541  dvlog  20542  efopnlem2  20548  efopn  20549  logccv  20554  dvsqr  20628  cxpcn3  20632  angpined  20671  1cubr  20682  atanre  20725  asinsin  20732  asin1  20734  reasinsin  20736  atan0  20748  atanbnd  20766  atan1  20768  log2cnv  20784  log2ublem3  20788  log2ub  20789  birthday  20793  amgmlem  20828  emcllem5  20838  emgt0  20845  harmonicbnd3  20846  ftalem3  20857  basellem4  20866  sgmf  20928  ppi1  20947  cht1  20948  vma1  20949  ppiltx  20960  sqff1o  20965  ppiublem1  20986  ppiublem2  20987  ppiub  20988  chtub  20996  dchreq  21042  bposlem7  21074  bposlem8  21075  bposlem9  21076  lgsdir2lem2  21108  lgsdir2lem3  21109  chebbnd1  21166  chto1ub  21170  chpo1ubb  21175  pntibndlem1  21283  umgrafi  21357  usgraexmpl  21420  usgrafilem1  21425  2trllemA  21550  wlkntrllem1  21559  wlkntrllem3  21561  0pth  21570  spthispth  21573  2pthon  21602  2pthon3v  21604  redwlk  21606  constr3trllem3  21639  constr3pthlem3  21644  konigsberg  21709  ex-dif  21731  ex-un  21732  ex-in  21733  ex-fl  21755  avril1  21757  ginvsn  21937  cnid  21939  mulid  21944  rngosn3  22014  vcoprnelem  22057  vcoprne  22058  vcex  22059  cnnvm  22174  ipasslem8  22338  ipasslem10  22340  hvsubf  22518  normlem1  22612  normlem6  22617  normlem7  22618  norm-ii-i  22639  norm3adifii  22650  hilid  22663  hlimf  22740  norm1exi  22752  hhssabloi  22762  hhssnv  22764  hhshsslem1  22767  shincli  22864  shsval2i  22889  shs0i  22951  chj0i  22957  chm1i  22958  chincli  22962  chdmm1i  22979  shjshsi  22994  chsup0  23050  h1de2bi  23056  spansnpji  23080  cmcmlem  23093  cmcmii  23099  cmcm2ii  23100  cmcm3ii  23101  pjidmi  23175  pjssmii  23183  pj0i  23195  pjocini  23200  mayetes3i  23232  df0op2  23255  hoaddcomi  23275  hoaddassi  23279  hocadddiri  23282  hocsubdiri  23283  hoaddid1i  23289  ho0coi  23291  hoid1i  23292  hoid1ri  23293  hodseqi  23297  honegsubi  23299  adj1o  23397  hoddii  23492  lnopunilem1  23513  lnopunilem2  23514  nmcopexi  23530  nmcopex  23532  nmcoplb  23533  nmcfnexi  23554  nmcfnex  23556  nmcfnlb  23557  adjbd1o  23588  adjcoi  23603  nmopcoadji  23604  opsqrlem6  23648  pjsdii  23658  pjddii  23659  pjidmcoi  23680  pjtoi  23682  pjin1i  23695  pjclem1  23698  stji1i  23745  largei  23770  reuxfr3d  23976  iuninc  24011  rinvf1o  24042  suppss2f  24049  xppreima  24059  ofoprabco  24079  funcnvmptOLD  24082  gtiso  24088  df1stres  24091  df2ndres  24092  snct  24103  dmct  24106  hashresfn  24156  ressplusf  24183  xrge0base  24207  xrge00  24208  xrge0neqmnf  24212  xrnarchi  24254  unicls  24301  sqsscirc1  24306  mhmhmeotmd  24313  rmulccn  24314  raddcn  24315  xrge0iifiso  24321  xrge0iifhmeo  24322  lmxrge0  24337  cnzh  24354  rezh  24355  qqh0  24368  qqh1  24369  qqhre  24386  rrhre  24387  rnlogblem  24399  log2le1  24407  ind1a  24418  esumnul  24443  esum0  24444  esumsn  24456  esumpfinvallem  24464  esumpfinvalf  24466  esumpcvgval  24468  sigaclfu2  24504  dmsigagen  24527  imambfm  24612  mbfmvolf  24616  br2base  24619  sibfof  24654  sitmcl  24663  probdif  24678  0rrv  24709  coinfliplem  24736  coinflipprob  24737  coinfliprv  24740  ballotlem2  24746  ballotlem4  24756  ballotlem5  24757  ballotlemi  24758  ballotlemiex  24759  ballotlemi1  24760  ballotlemii  24761  ballotlemsup  24762  ballotlemimin  24763  ballotlem1c  24765  ballotlemfrcn0  24787  ballotlemirc  24789  ballotlem7  24793  ballotth  24795  subfacf  24861  subfacp1lem1  24865  subfacp1lem5  24870  subfacp1lem6  24871  subfacval3  24875  erdszelem2  24878  erdszelem9  24885  erdszelem11  24887  kur14lem4  24895  iooscon  24934  iccllyscon  24937  ghomgrpilem1  25096  ghomgrpilem2  25097  circum  25111  axextprim  25150  axrepprim  25151  axunprim  25152  axinfprim  25155  axacprim  25156  inffz  25200  fz0n  25202  risefall0lem  25342  binomfallfaclem2  25356  setinds  25405  dfon2lem2  25411  dfon2lem4  25413  dfrdg2  25423  axextdfeq  25425  poseq  25528  wfrlem4  25541  frrlem4  25585  sltval2  25611  nosgnn0  25613  sltintdifex  25618  sltres  25619  sltsolem1  25623  bdayfo  25630  symdifV  25670  fobigcup  25745  snelsingles  25767  fullfunfnv  25791  fullfunfv  25792  dfrdg4  25795  rankaltopb  25824  axlowdimlem4  25884  axlowdimlem13  25893  axlowdimlem16  25896  axlowdim1  25898  axlowdim  25900  linedegen  26077  rank0  26111  rankeq1o  26112  hfuni  26125  nabi1i  26141  nabi2i  26142  limsucncmpi  26195  mblfinlem1  26243  mblfinlem2  26244  ovoliunnfl  26248  voliunnfl  26250  itg2addnclem  26256  itg2addnclem2  26257  dvreasin  26290  areacirclem1  26292  gtinf  26322  fneer  26368  neibastop1  26388  opelopab3  26418  fdc  26449  cntotbnd  26505  heiborlem6  26525  rrnval  26536  reheibor  26548  prter2  26730  diophrw  26817  0dioph  26837  rabren3dioph  26876  rencldnfilem  26881  pellexlem6  26897  pellex  26898  pellfundval  26943  frmx  26976  frmy  26977  jm2.23  27067  jm2.27dlem3  27082  axac10  27104  pw2f1ocnv  27108  wepwsolem  27116  kelac2lem  27139  lmhmlnmsplit  27162  dsmmbas2  27180  pwfi2f1o  27237  frlmpwfi  27239  dgraaval  27326  dgraaf  27329  symgsssg  27385  symgfisg  27386  psgnunilem5  27394  psgnghm  27414  seff  27515  expgrowthi  27527  expgrowth  27529  refsum2cnlem1  27684  infrglb  27698  dvcosre  27717  stoweidlem1  27726  stoweidlem7  27732  stoweidlem26  27751  stoweidlem34  27759  stoweidlem44  27769  stoweid  27788  stirlinglem5  27803  stirlinglem6  27804  axorbtnotaiffb  27847  axorbciffatcxorb  27849  abnotbtaxb  27860  resisresindm  28074  fzo0ss1  28123  swrd0fv0  28193  reumodprminv  28227  frgrawopreg2  28440  ee233  28602  a9e2nd  28645  in1  28662  dfvd2ani  28675  dfvd2i  28677  dfvd3i  28684  dfvd3ani  28687  e0bi  28888  uun2221  28925  uun2221p1  28926  uun2221p2  28927  en3lpVD  28957  relopabVD  29013  a9e2ndVD  29020  a9e2ndALT  29042  bnj521  29104  bnj1098  29154  bnj1109  29157  bnj1131  29158  bnj1533  29223  bnj151  29248  bnj580  29284  bnj852  29292  bnj864  29293  bnj865  29294  bnj978  29320  bnj1021  29335  bnj907  29336  bnj1093  29349  bnj1145  29362  bnj1172  29370  bnj1174  29372  bnj1176  29374  bnj1186  29376  sbcoNEW7  29582  sbidmNEW7  29584  sbcomOLD7  29755  sb9iOLD7  29758  mapdunirnN  32448
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 178
  Copyright terms: Public domain W3C validator