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

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

Proof of Theorem mpbir
StepHypRef Expression
1 mpbir.min . 2  |-  ps
2 mpbir.maj . . 3  |-  ( ph  <->  ps )
32biimpri 197 . 2  |-  ( ps 
->  ph )
41, 3ax-mp 8 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  pm5.74ri  237  con4bii  288  orri  365  imorri  403  imnani  412  mpbir2an  886  mpbir3an  1134  tru  1321  nic-mpALT  1437  nic-ax  1438  nic-axALT  1439  mpto2OLD  1535  mtp-xor  1536  mtp-xorOLD  1537  mpgbir  1550  nfxfr  1570  19.35ri  1602  a9ev  1656  exiftruOLD  1658  exan  1885  a9e  1956  cbval2  2009  cbvex2  2010  sbt  2038  moaneu  2268  moanmo  2269  axi12  2338  axext2  2340  eqeltri  2428  nfcxfr  2491  neirr  2526  exmidne  2527  eqnetri  2538  mprgbir  2689  vex  2867  issetri  2871  moeq  3017  cdeqi  3052  ru  3066  eqsstri  3284  3sstr4i  3293  tpid1  3815  tpid2  3816  tpid3  3818  pwv  3905  uni0  3933  eqbrtri  4121  tr0  4203  trv  4204  zfrep4  4218  zfnuleu  4225  axnulALT  4226  0ex  4229  inex1  4234  0elpw  4259  axpow2  4269  axpow3  4270  pwex  4272  dvdemo1  4289  zfpair2  4294  exss  4315  moop2  4340  pwundif  4379  po0  4408  epse  4455  0elon  4524  nsuceq0  4551  uniex2  4594  snnex  4603  tfinds2  4733  finds  4761  finds2  4763  relsnop  4870  relxp  4873  rel0  4889  relopabi  4890  eliunxp  4902  opeliunxp2  4903  dmi  4972  xpidtr  5144  cnvcnv  5205  dmsn0  5219  cnvsn0  5220  funmpt  5369  funmpt2  5370  isarep2  5411  fresaunres2  5493  f0  5505  f10  5587  f1o00  5588  f1oi  5591  f1osn  5593  brprcneu  5598  fvopab3ig  5679  opabex  5827  eufnfv  5835  mpt2fun  6030  reldmmpt2  6039  oprabex  6045  oprabex3  6046  ovid  6048  ovidig  6049  ovidi  6050  ovig  6053  ov3  6068  caovmo  6141  relmptopab  6149  f1stres  6225  f2ndres  6226  relmpt2opab  6285  tpos0  6348  porpss  6365  opabiotafun  6375  canth  6378  ncanth  6379  issmo  6449  tfrlem6  6482  tfrlem8  6484  tfrlem16  6493  tfr1a  6494  tfr1  6497  tz7.44lem1  6502  seqomlem2  6547  seqomlem3  6548  seqomlem4  6549  fnseqom  6551  abianfp  6555  0lt1o  6587  0we1  6589  eqer  6777  ecopover  6847  th3qcor  6851  mapsnf1o3  6901  ssdomg  6992  ensn1  7010  snfi  7026  xpcomf1o  7036  map2xp  7116  limensuci  7122  sdom1  7147  unblem4  7199  fidomdm  7225  marypha1lem  7273  hartogslem1  7344  hartogs  7346  card2on  7355  ruv  7401  ruALT  7402  inf2  7411  inf3lem6  7421  infeq5i  7424  zfinf2  7430  cantnflt  7460  cantnf  7482  mapfien  7486  cnfcom  7490  trcl  7497  tz9.1c  7499  tc2  7514  r1funlim  7525  r1fnon  7526  karden  7652  tskwe  7670  cardprclem  7699  cardprc  7700  pm54.43  7720  r0weon  7727  iunmapdisj  7737  alephfnon  7779  alephfplem4  7821  alephfp  7822  alephval3  7824  aceq3lem  7834  kmlem2  7864  cda1dif  7889  ackbij1  7951  ackbij2lem2  7953  ackbij2  7956  infpssrlem3  8018  hsmexlem4  8142  hsmexlem5  8143  axdc3lem4  8166  ac2  8174  axac3  8177  ac6  8194  axdclem2  8234  ondomon  8272  alephsucpw  8279  pwcfsdom  8292  cfpwsdom  8293  smobeth  8295  axpowndlem3  8308  zfcndun  8324  zfcndpow  8325  zfcndinf  8327  zfcndac  8328  wunex2  8447  uniwun  8449  wuncid  8452  wuncval2  8456  grur1  8529  axgroth5  8533  axgroth2  8534  axgroth6  8537  axgroth3  8540  grothtsk  8544  inaprc  8545  ltsopi  8599  dmaddpi  8601  dmmulpi  8602  1lt2pi  8616  nqerf  8641  addnqf  8659  mulnqf  8660  1lt2nq  8684  0r  8789  1sr  8790  m1r  8791  m1p1sr  8801  m1m1sr  8802  0lt1sr  8804  axaddf  8854  axmulf  8855  ax1cn  8858  ax1ne0  8869  pnfnre  8961  mnfnre  8962  subaddrii  9222  ine0  9302  ixi  9484  recgt0ii  9749  nn1suc  9854  4d2e2  9965  nnunb  10050  arch  10051  un0mulcl  10087  nummac  10245  uzf  10322  indstr  10376  mnfltpnf  10554  ixxf  10755  ioof  10830  fzf  10875  fzp1disj  10932  fzof  10961  om2uzrani  11104  om2uzf1oi  11105  uzrdglem  11109  uzrdgfni  11110  uzrdg0i  11111  ltwenn  11114  hashgf1o  11122  axdc4uzlem  11133  sq0  11285  irec  11292  hashkf  11429  hashf  11434  hash0  11445  hashsslei  11468  hashxplem  11475  hashbclem  11480  hashf1lem1  11483  wrd0  11508  wrdexg  11515  revs1  11573  cats1fvn  11598  climmo  12121  fsumcom2  12328  ackbijnn  12377  incexclem  12386  infcvgaux1i  12406  efcvgfsum  12458  cos1bnd  12558  cos2bnd  12559  eirr  12574  znnen  12582  qnnen  12583  aleph1re  12614  sqr2irr  12618  nthruz  12621  dvdslelem  12664  3dvds  12682  divalglem5  12687  bitsf  12709  sadcaddlem  12739  sadadd2lem  12741  sadadd3  12743  sadaddlem  12748  isprm3  12858  2prm  12865  3prm  12866  phicl2  12927  pockthi  13045  unbenlem  13046  prmrec  13060  vdwlem13  13131  vdwnn  13136  ramcl2  13154  mod2xnegi  13177  modsubi  13178  structcnvcnv  13250  structfun  13251  setsres  13265  strfv  13271  strlemor1  13326  strleun  13329  0rest  13427  firest  13430  restid  13431  prdsval  13448  prdsbas  13450  prdsplusg  13451  prdsmulr  13452  prdsvsca  13453  prdsds  13456  imasaddfnlem  13523  imasvscafn  13532  oppchomfval  13710  oppcbas  13714  2oppchomf  13720  rescbas  13799  rescco  13802  rescabs  13803  idfucl  13848  wunnat  13923  homarel  13961  dmaf  13974  cdaf  13975  dmcoass  13991  catcfuccl  14034  xpcbas  14045  relxpchom  14048  catcxpccl  14074  oppchofcl  14127  oyoncl  14137  odubas  14330  letsr  14442  mgmidmo  14463  releqg  14757  ga0  14845  oppglem  14916  efgval  15119  efger  15120  efgsp1  15139  efgsfo  15141  efgredleme  15145  efgredlem  15149  efgred  15150  cygctb  15271  gsum2d2lem  15317  gsum2d2  15318  gsumcom2  15319  dprd2d2  15372  pgpfaclem1  15409  mgplem  15423  mgpress  15429  opprlem  15503  reldvdsr  15519  00lsp  15831  sralem  16023  srasca  16027  psrvscafval  16228  opsrbaslem  16312  psrbag0  16328  00ply1bas  16411  ply1plusgfvi  16413  zlmsca  16575  znbaslem  16592  ocvfval  16666  ocv0  16677  cssval  16682  thlbas  16696  thlle  16697  eltopspOLD  16756  tgdom  16816  tgidm  16818  indistps2ALT  16851  restbas  16989  resttopon  16992  rest0  17000  leordtval2  17042  iocpnfordt  17045  icomnfordt  17046  iooordt  17047  cnpfval  17064  iscnp2  17069  ist1-3  17177  1stcfb  17271  islly2  17310  1stckgen  17349  ptbasfi  17376  xkotf  17380  dfac14  17412  opnfbas  17633  zfbas  17687  hauspwpwf1  17778  alexsubALTlem4  17840  alexsubALT  17841  ptcmplem5  17846  0met  18026  prdsdsf  18027  prdsxmetlem  18028  prdsmet  18030  setsmsbas  18117  setsmsds  18118  prdsbl  18133  tngds  18260  qtopbaslem  18363  xrtgioo  18408  xrsdsre  18412  zcld  18415  recld2  18416  sszcld  18419  reperflem  18420  retopcon  18431  iccpnfcnv  18540  bndth  18554  ishtpy  18568  nmoleub2lem2  18695  recmet  18843  resscdrg  18873  ishl2  18885  volf  18986  iundisj2  19004  volsup  19011  icombl  19019  ioombl  19020  ismbf3d  19107  0plef  19125  0pledm  19126  itg1ge0  19139  mbfi1fseqlem5  19172  itg2addlem  19211  iblcnlem1  19240  reldv  19318  limciun  19342  dvexp  19400  dveflem  19424  lhop1lem  19458  lhop  19461  elply2  19676  elplyd  19682  ply1term  19684  ply0  19688  plymullem  19696  qaa  19801  aaliou3  19829  pserulm  19899  pserdvlem2  19905  efcn  19920  sincosq1lem  19966  tangtx  19974  sincos4thpi  19982  sincos6thpi  19984  pige3  19986  efif1olem4  20008  logf1o  20023  relogf1o  20025  log1  20041  loge  20042  relogiso  20053  dvrelog  20089  relogcn  20090  logcn  20099  cxpcn3  20193  resqrcn  20194  leibpi  20343  log2ublem1  20347  birthday  20354  emcllem5  20399  harmonicbnd  20403  harmonicbnd2  20404  emgt0  20406  harmonicbnd3  20407  ppiltx  20521  ppiublem1  20547  ppiub  20549  bclbnd  20625  bpos1lem  20627  bposlem8  20636  lgsquadlem2  20700  2sqlem9  20718  2sqlem10  20719  chebbnd1  20727  selberg2lem  20805  pntrsumo1  20820  selbergsb  20830  pntpbnd  20843  ex-dif  20916  ex-in  20918  ex-eprel  20926  ex-id  20927  ex-fl  20940  avril1  20942  2bornot2b  20943  grposn  20988  issubgoi  21083  0vfval  21270  vsfval  21299  ajmoi  21545  ajfuni  21546  normlem2  21798  norm3adifii  21835  hhip  21864  hlim0  21923  hlimcaui  21924  hlimf  21925  hhssnv  21949  shscli  22004  shsval2i  22074  h1de2i  22240  fh3i  22310  fh4i  22311  cm2mi  22313  qlaxr3i  22323  mayetes3i  22417  ho0f  22439  hoif  22442  hodidi  22475  ho0subi  22483  hosd1i  22510  adjmo  22520  nmopsetn0  22553  nmfnsetn0  22566  funadj  22574  funcnvadj  22581  nmcexi  22714  cnlnadjlem8  22762  nmoptri2i  22787  opsqrlem4  22831  hmopidmchi  22839  pjoci  22868  pjinvari  22879  rabexgfGS  23177  abrexdomjm  23178  pwundif2  23194  elim2ifim  23202  iundisj2f  23225  xpima  23235  rinvf1o  23243  xppreima2  23260  funcnvmptOLD  23282  funcnvmpt  23283  snct  23304  dmct  23307  fzossnn  23351  iundisj2fi  23354  xrge0iifcnv  23475  xrge0pluscn  23482  cnextrel  23500  ust0  23523  tuslem  23565  recms  23619  zlmds  23623  zlmtset  23624  qqhre  23653  esumfsup  23726  esumpcvgval  23734  hasheuni  23741  esumcvg  23742  dmvlsiga  23778  dmsigagen  23793  brsiga  23803  brsigarn  23804  measbasedom  23821  measvuni  23832  voliune  23849  volfiniune  23850  br2base  23883  sxbrsigalem0  23885  dya2iocct  23894  dya2iocuni  23897  dya2iocucvr  23898  sxbrsiga  23904  coinflipprob  23986  coinfliprv  23989  coinflippvt  23991  ballotlem2  23995  ballotlemfc0  23999  ballotlemfcc  24000  ballotlem4  24005  ballotlemic  24013  ballotlem7  24042  ballotth  24044  lgamgulm2  24069  lgamcvglem  24073  gamf  24076  subfacp1lem5  24119  subfacp1lem6  24120  kur14lem9  24149  cvmcov2  24210  cvmliftlem1  24220  cvmliftlem4  24223  cvmliftlem5  24224  umgra0  24281  umgrabi  24311  vdegp1ai  24312  vdegp1bi  24313  konigsberg  24315  ghomgrpilem2  24397  relexp0  24429  relexpsucr  24430  relexpsucl  24432  dfrtrclrec2  24444  rtrclreclem.refl  24445  rtrclreclem.subset  24446  rtrclreclem.min  24448  dfrtrcl2  24449  brtpid1  24479  brtpid2  24480  brtpid3  24481  fzp1nel  24511  gamma1  24645  faclimlem1  24654  domep  24707  axextndbi  24719  poseq  24811  wfrlem14  24827  wfrlem16  24829  frrlem10  24850  sltval2  24868  nosgnn0i  24871  brv  24975  txprel  24977  relsset  24986  relbigcup  24995  fvbigcup  25000  fnsingle  25016  fvsingle  25017  snelsingles  25019  funimage  25025  fullfunfnv  25043  ax5seglem7  25122  axlowdimlem4  25132  axlowdimlem6  25134  axlowdimlem7  25135  axlowdimlem10  25138  axlowdimlem13  25141  axlowdimlem16  25144  axlowdimlem17  25145  axlowdim  25148  funtransport  25213  colinrel  25239  funray  25322  funline  25324  bpolylem  25342  bpoly3  25352  bpoly4  25353  0hf  25366  waj-ax  25412  lukshef-ax2  25413  arg-ax  25414  limsucncmpi  25443  voliunnfl  25490  itg2addnc  25494  itgaddnclem2  25499  comppfsc  25631  neibastop2lem  25633  filnetlem3  25653  cover2  25682  abrexdom  25729  fdc  25779  cncfres  25808  heibor1lem  25856  moxfr  26075  mapfzcons1  26117  diophrw  26161  0dioph  26181  vdioph  26182  ftp  26216  rabren3dioph  26221  2nn0ind  26353  rpnnen3  26448  kelac2lem  26485  frlmpwfi  26585  islinds2  26606  psgnunilem3  26742  psgnunilem4  26743  matsca  26793  lhe4.4ex1a  26869  rusbcALT  26962  compneOLD  26966  ipo0  26975  ifr0  26976  rfcnpre1  27013  fnchoice  27023  rrpsscn  27042  dvcosre  27064  stoweidlem5  27077  stoweidlem13  27085  stoweidlem26  27098  stoweidlem28  27100  stoweidlem34  27106  stoweidlem44  27116  stoweidlem59  27131  stoweid  27135  wallispilem3  27139  wallispilem4  27140  wallispi2lem1  27143  stirlinglem5  27150  stirlinglem13  27158  stirlinglem14  27159  stirlingr  27162  uhgra0  27508  usgra0  27537  usgra1v  27555  nbgraf1o0  27602  cusgraexilem2  27622  cusgrasizeindslem2  27629  0wlk  27680  0trl  27681  wlkntrllem2  27685  wlkntrllem3  27686  wlkntrllem4  27687  0pth  27695  1pthonlem1  27708  usgrcyclnl2  27748  4cycl4dv  27774  vdgref  27788  frgra0  27810  ex-gte  27882  AnelBC  27917  vk15.4j  28019  2sb5nd  28054  dfvd1ir  28069  dfvd2anir  28081  dfvd2ir  28083  dfvd3ir  28090  dfvd3anir  28093  iden2  28120  e0bir  28295  uun2221p1  28332  uun2221p2  28333  2sb5ndVD  28431  2sb5ndALT  28454  bnj226  28507  bnj1101  28561  bnj110  28635  bnj149  28652  bnj150  28653  bnj151  28654  bnj517  28662  bnj580  28690  bnj865  28700  bnj900  28706  bnj996  28732  bnj1110  28757  bnj1133  28764  bnj1128  28765  bnj1145  28768  bnj1137  28770  bnj1171  28775  bnj1176  28780  a9eNEW7  28876  sbtNEW7  29032  cbval2OLD7  29114  cbvex2OLD7  29115  nfsb4tw2AUXOLD7  29130  ax12conj2  29160  a12stdy1-x12  29163  a12study10  29188  a12study10n  29189  hlhilslem  32183
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