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

Theorem mpbir 201
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 198 . 2  |-  ( ps 
->  ph )
41, 3ax-mp 8 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  pm5.74ri  238  con4bii  289  orri  366  imorri  404  imnani  413  mpbir2an  887  mpbir3an  1136  tru  1330  nic-mpALT  1446  nic-ax  1447  nic-axALT  1448  mpto2OLD  1544  mtp-xor  1545  mtp-xorOLD  1546  mpgbir  1559  nfxfr  1579  19.35ri  1612  a9ev  1668  exiftruOLD  1670  exan  1903  cbval2OLD  1990  cbvex2  1991  ax12  2019  a9eOLD  2034  sbt  2112  moaneu  2339  moanmo  2340  axi12  2409  axext2  2412  eqeltri  2500  nfcxfr  2563  neirr  2598  exmidne  2599  eqnetri  2610  mprgbir  2763  vex  2946  issetri  2950  moeq  3097  cdeqi  3133  ru  3147  eqsstri  3365  3sstr4i  3374  tpid1  3904  tpid2  3905  tpid3  3907  pwv  4001  uni0  4029  eqbrtri  4218  tr0  4300  trv  4301  zfrep4  4315  zfnuleu  4322  axnulALT  4323  0ex  4326  inex1  4331  0elpw  4356  axpow2  4366  axpow3  4367  pwex  4369  dvdemo1  4386  zfpair2  4391  exss  4413  moop2  4438  pwundif  4477  po0  4505  epse  4552  0elon  4621  nsuceq0  4648  uniex2  4690  snnex  4699  tfinds2  4829  finds  4857  finds2  4859  relsnop  4966  relxp  4969  rel0  4985  relopabi  4986  eliunxp  4998  opeliunxp2  4999  dmi  5070  xpidtr  5242  xpima  5299  cnvcnv  5309  dmsn0  5323  cnvsn0  5324  funmpt  5475  funmpt2  5476  isarep2  5519  fresaunres2  5601  f0  5613  f10  5695  f1o00  5696  f1oi  5699  f1osn  5701  brprcneu  5707  fvopab3ig  5789  opabex  5950  eufnfv  5958  mpt2fun  6158  reldmmpt2  6167  oprabex  6173  oprabex3  6174  ovid  6176  ovidig  6177  ovidi  6178  ovig  6181  ov3  6196  caovmo  6270  relmptopab  6278  f1stres  6354  f2ndres  6355  relmpt2opab  6415  tpos0  6495  porpss  6512  opabiotafun  6522  canth  6525  ncanth  6526  issmo  6596  tfrlem6  6629  tfrlem8  6631  tfrlem16  6640  tfr1a  6641  tfr1  6644  tz7.44lem1  6649  seqomlem2  6694  seqomlem3  6695  seqomlem4  6696  fnseqom  6698  abianfp  6702  0lt1o  6734  0we1  6736  eqer  6924  ecopover  6994  th3qcor  6998  mapsnf1o3  7048  ssdomg  7139  ensn1  7157  snfi  7173  xpcomf1o  7183  map2xp  7263  limensuci  7269  sdom1  7294  unblem4  7348  fidomdm  7374  marypha1lem  7424  hartogslem1  7495  hartogs  7497  card2on  7506  ruv  7552  ruALT  7553  inf2  7562  inf3lem6  7572  infeq5i  7575  zfinf2  7581  cantnflt  7611  cantnf  7633  mapfien  7637  cnfcom  7641  trcl  7648  tz9.1c  7650  tc2  7665  r1funlim  7676  r1fnon  7677  karden  7803  tskwe  7821  cardprclem  7850  cardprc  7851  pm54.43  7871  r0weon  7878  iunmapdisj  7888  alephfnon  7930  alephfplem4  7972  alephfp  7973  alephval3  7975  aceq3lem  7985  kmlem2  8015  cda1dif  8040  ackbij1  8102  ackbij2lem2  8104  ackbij2  8107  infpssrlem3  8169  hsmexlem4  8293  hsmexlem5  8294  axdc3lem4  8317  ac2  8325  axac3  8328  ac6  8344  axdclem2  8384  ondomon  8422  alephsucpw  8429  pwcfsdom  8442  cfpwsdom  8443  smobeth  8445  axpowndlem3  8458  zfcndun  8474  zfcndpow  8475  zfcndinf  8477  zfcndac  8478  wunex2  8597  uniwun  8599  wuncval2  8606  grur1  8679  axgroth5  8683  axgroth2  8684  axgroth6  8687  axgroth3  8690  grothtsk  8694  inaprc  8695  ltsopi  8749  dmaddpi  8751  dmmulpi  8752  1lt2pi  8766  nqerf  8791  addnqf  8809  mulnqf  8810  1lt2nq  8834  m1p1sr  8951  m1m1sr  8952  0lt1sr  8954  axaddf  9004  axmulf  9005  ax1cn  9008  ax1ne0  9019  pnfnre  9111  mnfnre  9112  subaddrii  9373  ine0  9453  ixi  9635  recgt0ii  9900  nn1suc  10005  4d2e2  10116  nnunb  10201  arch  10202  un0mulcl  10238  nummac  10398  uzf  10475  indstr  10529  mnfltpnf  10707  ixxf  10910  ioof  10986  fzf  11031  fzp1disj  11089  fzof  11120  om2uzrani  11275  om2uzf1oi  11276  uzrdglem  11280  uzrdgfni  11281  uzrdg0i  11282  ltwenn  11285  hashgf1o  11293  axdc4uzlem  11304  sq0  11456  irec  11463  hashkf  11603  hashf  11608  hash0  11629  hashsslei  11668  hashxplem  11679  hashbclem  11684  hashf1lem1  11687  wrd0  11715  wrdexg  11722  revs1  11780  cats1fvn  11805  climmo  12334  fsumcom2  12541  ackbijnn  12590  incexclem  12599  infcvgaux1i  12619  efcvgfsum  12671  cos1bnd  12771  cos2bnd  12772  eirr  12787  znnen  12795  qnnen  12796  aleph1re  12827  sqr2irr  12831  nthruz  12834  dvdslelem  12877  3dvds  12895  divalglem5  12900  bitsf  12922  sadcaddlem  12952  sadadd2lem  12954  sadadd3  12956  sadaddlem  12961  isprm3  13071  2prm  13078  phicl2  13140  pockthi  13258  unbenlem  13259  prmrec  13273  vdwlem13  13344  vdwnn  13349  ramcl2  13367  mod2xnegi  13390  modsubi  13391  structcnvcnv  13463  structfun  13464  setsres  13478  strfv  13484  strlemor1  13539  strleun  13542  0rest  13640  firest  13643  restid  13644  prdsval  13661  prdsbas  13663  prdsplusg  13664  prdsmulr  13665  prdsvsca  13666  prdsds  13669  imasaddfnlem  13736  imasvscafn  13745  oppchomfval  13923  oppcbas  13927  2oppchomf  13933  rescbas  14012  rescco  14015  rescabs  14016  idfucl  14061  wunnat  14136  homarel  14174  dmaf  14187  cdaf  14188  catcfuccl  14247  relxpchom  14261  catcxpccl  14287  oppchofcl  14340  oyoncl  14350  odubas  14543  letsr  14655  mgmidmo  14676  releqg  14970  ga0  15058  oppglem  15129  efgval  15332  efger  15333  efgsp1  15352  efgsfo  15354  efgredleme  15358  efgredlem  15362  efgred  15363  cygctb  15484  gsum2d2lem  15530  gsum2d2  15531  gsumcom2  15532  dprd2d2  15585  pgpfaclem1  15622  mgplem  15636  mgpress  15642  opprlem  15716  reldvdsr  15732  00lsp  16040  sralem  16232  srasca  16236  psrvscafval  16437  opsrbaslem  16521  psrbag0  16537  00ply1bas  16617  ply1plusgfvi  16619  zlmsca  16785  znbaslem  16802  ocvfval  16876  ocv0  16887  cssval  16892  thlbas  16906  thlle  16907  eltopspOLD  16966  tgdom  17026  tgidm  17028  indistps2ALT  17061  restbas  17205  resttopon  17208  rest0  17216  leordtval2  17259  iocpnfordt  17262  icomnfordt  17263  iooordt  17264  cnpfval  17281  iscnp2  17286  ist1-3  17396  1stcfb  17491  islly2  17530  1stckgen  17569  ptbasfi  17596  xkotf  17600  dfac14  17633  opnfbas  17857  zfbas  17911  hauspwpwf1  18002  alexsubALTlem4  18064  alexsubALT  18065  ptcmplem5  18070  cnextrel  18077  ust0  18232  tuslem  18280  0met  18379  prdsdsf  18380  prdsxmetlem  18381  prdsmet  18383  setsmsbas  18488  setsmsds  18489  prdsbl  18504  tngds  18672  qtopbaslem  18775  xrtgioo  18820  xrsdsre  18824  zcld  18827  recld2  18828  sszcld  18831  reperflem  18832  retopcon  18843  iccpnfcnv  18952  bndth  18966  ishtpy  18980  nmoleub2lem2  19107  recmet  19259  resscdrg  19295  ishl2  19307  volf  19408  iundisj2  19426  volsup  19433  icombl  19441  ioombl  19442  ismbf3d  19529  0plef  19547  0pledm  19548  itg1ge0  19561  mbfi1fseqlem5  19594  itg2addlem  19633  iblcnlem1  19662  reldv  19740  limciun  19764  dvexp  19822  dveflem  19846  lhop1lem  19880  lhop  19883  elply2  20098  elplyd  20104  ply1term  20106  ply0  20110  plymullem  20118  qaa  20223  aaliou3  20251  pserulm  20321  pserdvlem2  20327  efcn  20342  sincosq1lem  20388  tangtx  20396  sincos4thpi  20404  sincos6thpi  20406  pige3  20408  efif1olem4  20430  logf1o  20445  relogf1o  20447  log1  20463  loge  20464  relogiso  20475  dvrelog  20511  relogcn  20512  logcn  20521  cxpcn3  20615  resqrcn  20616  leibpi  20765  log2ublem1  20769  birthday  20776  emcllem5  20821  harmonicbnd  20825  harmonicbnd2  20826  emgt0  20828  harmonicbnd3  20829  ppiltx  20943  ppiublem1  20969  ppiub  20971  bclbnd  21047  bpos1lem  21049  bposlem8  21058  lgsquadlem2  21122  2sqlem9  21140  2sqlem10  21141  chebbnd1  21149  selberg2lem  21227  pntrsumo1  21242  selbergsb  21252  pntpbnd  21265  uhgra0  21327  umgra0  21343  usgra0  21373  usgra1v  21392  cusgraexilem2  21459  cusgrasizeindslem2  21466  0wlk  21528  0trl  21529  wlkntrllem2  21543  wlkntrl  21545  0pth  21553  1pthonlem1  21572  usgrcyclnl2  21611  4cycl4dv  21637  vdgrf  21652  umgrabi  21688  vdegp1ai  21689  vdegp1bi  21690  konigsberg  21692  ex-dif  21714  ex-in  21716  ex-eprel  21724  ex-id  21725  ex-fl  21738  avril1  21740  2bornot2b  21741  grposn  21786  issubgoi  21881  0vfval  22068  vsfval  22097  ajmoi  22343  ajfuni  22344  normlem2  22596  norm3adifii  22633  hhip  22662  hlim0  22721  hlimcaui  22722  hlimf  22723  hhssnv  22747  shscli  22802  shsval2i  22872  h1de2i  23038  fh3i  23108  fh4i  23109  cm2mi  23111  qlaxr3i  23121  mayetes3i  23215  ho0f  23237  hoif  23240  hodidi  23273  ho0subi  23281  hosd1i  23308  adjmo  23318  nmopsetn0  23351  nmfnsetn0  23364  funadj  23372  funcnvadj  23379  nmcexi  23512  cnlnadjlem8  23560  nmoptri2i  23585  opsqrlem4  23629  hmopidmchi  23637  pjoci  23666  pjinvari  23677  abrexdomjm  23971  elim2ifim  23989  iundisj2f  24013  rinvf1o  24025  funcnvmptOLD  24065  snct  24086  dmct  24089  iundisj2fi  24136  xrge0iifcnv  24302  xrge0pluscn  24309  recms  24326  zlmds  24331  zlmtset  24332  cnzh  24337  rezh  24338  qqhre  24369  esumfsup  24443  esumpcvgval  24451  hasheuni  24458  esumcvg  24459  dmsigagen  24510  measvuni  24551  voliune  24568  volfiniune  24569  br2base  24602  dya2iocuni  24616  coinfliprv  24723  ballotlem2  24729  ballotlemfc0  24733  ballotlemfcc  24734  ballotlemic  24747  ballotlem7  24776  ballotth  24778  lgamgulm2  24803  lgamcvglem  24807  gamf  24810  subfacp1lem5  24853  subfacp1lem6  24854  kur14lem9  24883  cvmcov2  24945  cvmliftlem1  24955  cvmliftlem4  24958  cvmliftlem5  24959  ghomgrpilem2  25080  relexp0  25112  relexpsucr  25113  relexpsucl  25115  dfrtrclrec2  25126  rtrclreclem.refl  25127  rtrclreclem.subset  25128  rtrclreclem.min  25130  dfrtrcl2  25131  brtpid1  25161  brtpid2  25162  brtpid3  25163  fzp1nel  25193  fprodcom2  25292  faclimlem1  25346  domep  25399  axextndbi  25411  poseq  25503  wfrlem14  25519  wfrlem16  25521  frrlem10  25542  sltval2  25560  nosgnn0i  25563  brv  25667  txprel  25669  relsset  25678  relbigcup  25687  fvbigcup  25692  fnsingle  25709  fvsingle  25710  snelsingles  25712  funimage  25718  fullfunfnv  25736  imagesset  25743  ax5seglem7  25817  axlowdimlem4  25827  axlowdimlem6  25829  axlowdimlem7  25830  axlowdimlem10  25833  axlowdimlem13  25836  axlowdimlem16  25839  axlowdimlem17  25840  axlowdim  25843  funtransport  25908  colinrel  25934  funray  26017  funline  26019  bpolylem  26037  bpoly3  26047  bpoly4  26048  0hf  26061  waj-ax  26107  lukshef-ax2  26108  arg-ax  26109  limsucncmpi  26138  mblfinlem  26185  ismblfin  26188  voliunnfl  26191  cnambfre  26196  comppfsc  26319  neibastop2lem  26321  filnetlem3  26341  cover2  26347  abrexdom  26364  fdc  26381  cncfres  26406  heibor1lem  26450  moxfr  26665  mapfzcons1  26705  diophrw  26749  0dioph  26769  vdioph  26770  rabren3dioph  26808  2nn0ind  26940  rpnnen3  27035  kelac2lem  27072  frlmpwfi  27172  islinds2  27193  psgnunilem3  27329  psgnunilem4  27330  matsca  27380  lhe4.4ex1a  27456  rusbcALT  27549  ipo0  27561  ifr0  27562  fnchoice  27609  stoweidlem13  27671  stoweidlem34  27692  stirlinglem5  27736  stirlinglem13  27744  stirlingr  27748  aistia  27774  aisfina  27775  aiffnbandciffatnotciffb  27781  axorbciffatcxorb  27782  abnotbtaxb  27793  abnotataxb  27794  usgra2pthspth  28077  usgra2pthlem1  28082  frgra0  28140  ex-gte  28228  AnelBC  28263  vk15.4j  28365  2sb5nd  28400  dfvd1ir  28416  dfvd2anir  28428  dfvd2ir  28430  dfvd3ir  28437  dfvd3anir  28440  iden2  28467  e0bir  28641  uun2221p1  28678  uun2221p2  28679  2sb5ndVD  28774  2sb5ndALT  28797  iunconlem2  28800  bnj226  28853  bnj1101  28907  bnj110  28981  bnj149  28998  bnj150  28999  bnj151  29000  bnj517  29008  bnj580  29036  bnj865  29046  bnj900  29052  bnj996  29078  bnj1110  29103  bnj1133  29110  bnj1128  29111  bnj1145  29114  bnj1137  29116  bnj1171  29121  bnj1176  29126  a9eNEW7  29222  sbtNEW7  29378  cbval2OLD7  29460  cbvex2OLD7  29461  nfsb4tw2AUXOLD7  29476  hlhilslem  32470
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