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  1312  nic-mpALT  1427  nic-ax  1428  nic-axALT  1429  mpto2OLD  1525  mtp-xor  1526  mtp-xorOLD  1527  mpgbir  1540  nfxfr  1560  19.35ri  1592  a9ev  1646  exiftru  1647  a9e  1904  cbval2  1957  cbvex2  1958  sbt  1986  moaneu  2215  moanmo  2216  axext2  2278  eqeltri  2366  nfcxfr  2429  neirr  2464  exmidne  2465  eqnetri  2476  mprgbir  2626  vex  2804  issetri  2808  moeq  2954  cdeqi  2989  ru  3003  eqsstri  3221  3sstr4i  3230  tpid1  3752  tpid2  3753  tpid3  3755  pwv  3842  uni0  3870  eqbrtri  4058  tr0  4140  trv  4141  zfrep4  4155  zfnuleu  4162  axnulALT  4163  0ex  4166  inex1  4171  0elpw  4196  axpow2  4206  axpow3  4207  pwex  4209  dvdemo1  4226  zfpair2  4231  exss  4252  moop2  4277  pwundif  4316  po0  4345  epse  4392  0elon  4461  nsuceq0  4488  uniex2  4531  snnex  4540  tfinds2  4670  finds  4698  finds2  4700  relsnop  4807  relxp  4810  rel0  4826  relopabi  4827  eliunxp  4839  opeliunxp2  4840  dmi  4909  xpidtr  5081  cnvcnv  5142  dmsn0  5156  cnvsn0  5157  funmpt  5306  funmpt2  5307  isarep2  5348  fresaunres2  5429  f0  5441  f10  5523  f1o00  5524  f1oi  5527  f1osn  5529  brprcneu  5534  fvopab3ig  5615  opabex  5760  eufnfv  5768  mpt2fun  5962  reldmmpt2  5971  oprabex  5977  oprabex3  5978  ovid  5980  ovidig  5981  ovidi  5982  ovig  5985  ov3  6000  caovmo  6073  relmptopab  6081  f1stres  6157  f2ndres  6158  relmpt2opab  6217  tpos0  6280  porpss  6297  opabiotafun  6307  canth  6310  ncanth  6311  issmo  6381  tfrlem6  6414  tfrlem8  6416  tfrlem16  6425  tfr1a  6426  tfr1  6429  tz7.44lem1  6434  seqomlem2  6479  seqomlem3  6480  seqomlem4  6481  fnseqom  6483  abianfp  6487  0lt1o  6519  0we1  6521  eqer  6709  ecopover  6778  th3qcor  6782  mapsnf1o3  6832  ssdomg  6923  ensn1  6941  snfi  6957  xpcomf1o  6967  map2xp  7047  limensuci  7053  sdom1  7078  unblem4  7128  fidomdm  7154  marypha1lem  7202  hartogslem1  7273  hartogs  7275  card2on  7284  ruv  7330  ruALT  7331  inf2  7340  inf3lem6  7350  infeq5i  7353  zfinf2  7359  cantnflt  7389  cantnf  7411  mapfien  7415  cnfcom  7419  trcl  7426  tz9.1c  7428  tc2  7443  r1funlim  7454  r1fnon  7455  karden  7581  tskwe  7599  cardprclem  7628  cardprc  7629  pm54.43  7649  r0weon  7656  iunmapdisj  7666  alephfnon  7708  alephfplem4  7750  alephfp  7751  alephval3  7753  aceq3lem  7763  kmlem2  7793  cda1dif  7818  ackbij1  7880  ackbij2lem2  7882  ackbij2  7885  infpssrlem3  7947  hsmexlem4  8071  hsmexlem5  8072  axdc3lem4  8095  ac2  8103  axac3  8106  ac6  8123  axdclem2  8163  ondomon  8201  alephsucpw  8208  pwcfsdom  8221  cfpwsdom  8222  smobeth  8224  axpowndlem3  8237  zfcndun  8253  zfcndpow  8254  zfcndinf  8256  zfcndac  8257  wunex2  8376  uniwun  8378  wuncid  8381  wuncval2  8385  grur1  8458  axgroth5  8462  axgroth2  8463  axgroth6  8466  axgroth3  8469  grothtsk  8473  inaprc  8474  ltsopi  8528  dmaddpi  8530  dmmulpi  8531  1lt2pi  8545  nqerf  8570  addnqf  8588  mulnqf  8589  1lt2nq  8613  0r  8718  1sr  8719  m1r  8720  m1p1sr  8730  m1m1sr  8731  0lt1sr  8733  axaddf  8783  axmulf  8784  ax1cn  8787  ax1ne0  8798  pnfnre  8890  mnfnre  8891  subaddrii  9151  ine0  9231  ixi  9413  recgt0ii  9678  nn1suc  9783  4d2e2  9892  nnunb  9977  arch  9978  un0mulcl  10014  nummac  10172  uzf  10249  indstr  10303  mnfltpnf  10481  ixxf  10682  ioof  10757  fzf  10802  fzp1disj  10859  fzof  10888  om2uzrani  11031  om2uzf1oi  11032  uzrdglem  11036  uzrdgfni  11037  uzrdg0i  11038  ltwenn  11041  hashgf1o  11049  axdc4uzlem  11060  sq0  11211  irec  11218  hashkf  11355  hashf  11360  hash0  11371  hashsslei  11394  hashxplem  11401  hashbclem  11406  hashf1lem1  11409  wrd0  11434  wrdexg  11441  revs1  11499  cats1fvn  11524  climmo  12047  fsumcom2  12253  ackbijnn  12302  incexclem  12311  infcvgaux1i  12331  efcvgfsum  12383  cos1bnd  12483  cos2bnd  12484  eirr  12499  znnen  12507  qnnen  12508  aleph1re  12539  sqr2irr  12543  nthruz  12546  dvdslelem  12589  3dvds  12607  divalglem5  12612  bitsf  12634  sadcaddlem  12664  sadadd2lem  12666  sadadd3  12668  sadaddlem  12673  isprm3  12783  2prm  12790  3prm  12791  phicl2  12852  pockthi  12970  unbenlem  12971  prmrec  12985  vdwlem13  13056  vdwnn  13061  ramcl2  13079  mod2xnegi  13102  modsubi  13103  structcnvcnv  13175  structfun  13176  setsres  13190  strfv  13196  strlemor1  13251  strleun  13254  0rest  13350  firest  13353  restid  13354  prdsval  13371  prdsbas  13373  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  prdsds  13379  imasaddfnlem  13446  imasvscafn  13455  oppchomfval  13633  oppcbas  13637  2oppchomf  13643  rescbas  13722  rescco  13725  rescabs  13726  idfucl  13771  wunnat  13846  homarel  13884  dmaf  13897  cdaf  13898  dmcoass  13914  catcfuccl  13957  xpcbas  13968  relxpchom  13971  catcxpccl  13997  oppchofcl  14050  oyoncl  14060  odubas  14253  letsr  14365  mgmidmo  14386  releqg  14680  ga0  14768  oppglem  14839  efgval  15042  efger  15043  efgsp1  15062  efgsfo  15064  efgredleme  15068  efgredlem  15072  efgred  15073  cygctb  15194  gsum2d2lem  15240  gsum2d2  15241  gsumcom2  15242  dprd2d2  15295  pgpfaclem1  15332  mgplem  15346  mgpress  15352  opprlem  15426  reldvdsr  15442  00lsp  15754  sralem  15946  srasca  15950  psrvscafval  16151  opsrbaslem  16235  psrbag0  16251  00ply1bas  16334  ply1plusgfvi  16336  zlmsca  16491  znbaslem  16508  ocvfval  16582  ocv0  16593  cssval  16598  thlbas  16612  thlle  16613  eltopspOLD  16672  tgdom  16732  tgidm  16734  indistps2ALT  16767  restbas  16905  resttopon  16908  rest0  16916  leordtval2  16958  iocpnfordt  16961  icomnfordt  16962  iooordt  16963  cnpfval  16980  iscnp2  16985  ist1-3  17093  1stcfb  17187  islly2  17226  1stckgen  17265  ptbasfi  17292  xkotf  17296  dfac14  17328  opnfbas  17553  zfbas  17607  hauspwpwf1  17698  alexsubALTlem4  17760  alexsubALT  17761  ptcmplem5  17766  0met  17946  prdsdsf  17947  prdsxmetlem  17948  prdsmet  17950  setsmsbas  18037  setsmsds  18038  prdsbl  18053  tngds  18180  qtopbaslem  18283  xrtgioo  18328  xrsdsre  18332  zcld  18335  recld2  18336  reperflem  18339  retopcon  18350  iccpnfcnv  18458  bndth  18472  ishtpy  18486  nmoleub2lem2  18613  recmet  18761  resscdrg  18791  ishl2  18803  volf  18904  iundisj2  18922  volsup  18929  icombl  18937  ioombl  18938  ismbf3d  19025  0plef  19043  0pledm  19044  itg1ge0  19057  mbfi1fseqlem5  19090  itg2addlem  19129  iblcnlem1  19158  reldv  19236  limciun  19260  dvexp  19318  dveflem  19342  lhop1lem  19376  lhop  19379  elply2  19594  elplyd  19600  ply1term  19602  ply0  19606  plymullem  19614  qaa  19719  aaliou3  19747  pserulm  19814  pserdvlem2  19820  efcn  19835  sincosq1lem  19881  tangtx  19889  sincos4thpi  19897  sincos6thpi  19899  pige3  19901  efif1olem4  19923  logf1o  19938  relogf1o  19940  log1  19955  loge  19956  relogiso  19967  dvrelog  20000  relogcn  20001  logcn  20010  cxpcn3  20104  resqrcn  20105  leibpi  20254  log2ublem1  20258  birthday  20265  emcllem5  20309  harmonicbnd  20313  harmonicbnd2  20314  emgt0  20316  harmonicbnd3  20317  ppiltx  20431  ppiublem1  20457  ppiub  20459  bclbnd  20535  bpos1lem  20537  bposlem8  20546  lgsquadlem2  20610  2sqlem9  20628  2sqlem10  20629  chebbnd1  20637  selberg2lem  20715  pntrsumo1  20730  selbergsb  20740  pntpbnd  20753  ex-dif  20826  ex-in  20828  ex-eprel  20836  ex-id  20837  ex-fl  20850  avril1  20852  2bornot2b  20853  grposn  20898  issubgoi  20993  0vfval  21178  vsfval  21207  ajmoi  21453  ajfuni  21454  normlem2  21706  norm3adifii  21743  hhip  21772  hlim0  21831  hlimcaui  21832  hlimf  21833  hhssnv  21857  shscli  21912  shsval2i  21982  h1de2i  22148  fh3i  22218  fh4i  22219  cm2mi  22221  qlaxr3i  22231  mayetes3i  22325  ho0f  22347  hoif  22350  hodidi  22383  ho0subi  22391  hosd1i  22418  adjmo  22428  nmopsetn0  22461  nmfnsetn0  22474  funadj  22482  funcnvadj  22489  nmcexi  22622  cnlnadjlem8  22670  nmoptri2i  22695  opsqrlem4  22739  hmopidmchi  22747  pjoci  22776  pjinvari  22787  rinvf1o  23054  ballotlem2  23063  ballotlemfc0  23067  ballotlemfcc  23068  ballotlem4  23073  ballotlemic  23081  ballotlem7  23110  ballotth  23112  elim2ifim  23169  abrexdomjm  23181  rabexgfGS  23187  pwundif2  23202  xpima  23217  xppreima2  23227  funcnvmptOLD  23249  funcnvmpt  23250  fzossnn  23293  xrge0iifcnv  23330  xrge0pluscn  23337  snct  23354  dmct  23357  iundisj2fi  23379  iundisj2f  23381  esumpcvgval  23461  hasheuni  23468  esumcvg  23469  dmvlsiga  23505  dmsigagen  23520  brsiga  23529  brsigarn  23530  measbasedom  23547  measvuni  23557  br2base  23589  coinflipprob  23695  coinfliprv  23698  coinflippvt  23700  subfacp1lem5  23730  subfacp1lem6  23731  kur14lem9  23760  cvmcov2  23821  cvmliftlem1  23831  cvmliftlem4  23834  cvmliftlem5  23835  umgra0  23892  umgrabi  23922  vdegp1ai  23923  vdegp1bi  23924  konigsberg  23926  ghomgrpilem2  24008  relexp0  24040  relexpsucr  24041  relexpsucl  24043  dfrtrclrec2  24055  rtrclreclem.refl  24056  rtrclreclem.subset  24057  rtrclreclem.min  24059  dfrtrcl2  24060  brtpid1  24090  brtpid2  24091  brtpid3  24092  domep  24219  axextndbi  24231  poseq  24323  wfrlem14  24339  wfrlem16  24341  frrlem10  24362  sltval2  24380  nosgnn0i  24383  brv  24487  txprel  24489  relsset  24498  relbigcup  24507  fvbigcup  24512  fnsingle  24528  fvsingle  24529  snelsingles  24531  funimage  24537  fullfunfnv  24555  ax5seglem7  24634  axlowdimlem4  24644  axlowdimlem6  24646  axlowdimlem7  24647  axlowdimlem10  24650  axlowdimlem13  24653  axlowdimlem16  24656  axlowdimlem17  24657  axlowdim  24660  funtransport  24725  colinrel  24751  funray  24834  funline  24836  bpolylem  24854  bpoly3  24864  bpoly4  24865  0hf  24878  waj-ax  24924  lukshef-ax2  24925  arg-ax  24926  limsucncmpi  24955  itg2addnc  25004  itgaddnclem2  25009  vxveqv  25156  prj1b  25181  prj3  25182  inposet  25380  dominc  25382  rninc  25383  zintdom  25540  basexre  25624  intopcoaconlem3  25641  cntrset  25704  1ded  25840  relded  25842  reldded  25843  relrded  25844  relcat  25863  reldcat  25864  relrcat  25865  phckle  26129  psckle  26130  fnckle  26147  pfsubkl  26149  pvp  26150  pgapspf  26154  pgapspf2  26155  comppfsc  26409  neibastop2lem  26411  filnetlem3  26431  cover2  26460  abrexdom  26507  fdc  26557  cncfres  26587  heibor1lem  26635  moxfr  26854  mapfzcons1  26896  diophrw  26940  0dioph  26960  vdioph  26961  ftp  26995  rabren3dioph  27000  2nn0ind  27132  rpnnen3  27227  kelac2lem  27264  frlmpwfi  27364  islinds2  27385  psgnunilem3  27521  psgnunilem4  27522  matsca  27572  lhe4.4ex1a  27648  rusbcALT  27741  compneOLD  27745  ipo0  27754  ifr0  27755  rfcnpre1  27792  fnchoice  27802  rrpsscn  27821  dvcosre  27843  stoweidlem5  27856  stoweidlem13  27864  stoweidlem26  27877  stoweidlem28  27879  stoweidlem34  27885  stoweidlem44  27895  stoweidlem59  27910  stoweid  27914  wallispilem3  27918  wallispilem4  27919  wallispi2lem1  27922  stirlinglem5  27929  stirlinglem13  27937  stirlinglem14  27938  stirlingr  27941  usgra0  28249  usgra1v  28259  usgraex0elv  28261  usgraex1elv  28262  usgraex2elv  28263  usgraex3elv  28264  0wlk  28342  0trl  28343  wlkntrllem2  28345  wlkntrllem3  28346  wlkntrllem4  28347  0pth  28355  usgrcyclnl2  28386  4cycl4dv  28412  frgra0  28420  ex-gte  28452  AnelBC  28487  vk15.4j  28589  2sb5nd  28624  dfvd1ir  28639  dfvd2anir  28651  dfvd2ir  28653  dfvd3ir  28660  dfvd3anir  28663  iden2  28690  e0bir  28865  uun2221p1  28902  uun2221p2  28903  2sb5ndVD  29001  2sb5ndALT  29024  bnj226  29077  bnj1101  29131  bnj110  29205  bnj149  29222  bnj150  29223  bnj151  29224  bnj517  29232  bnj580  29260  bnj865  29270  bnj900  29276  bnj996  29302  bnj1110  29327  bnj1133  29334  bnj1128  29335  bnj1145  29338  bnj1137  29340  bnj1171  29345  bnj1176  29350  a9eNEW7  29446  sbtNEW7  29602  cbval2OLD7  29684  cbvex2OLD7  29685  nfsb4tw2AUXOLD7  29700  ax12conj2  29730  a12stdy1-x12  29733  a12study10  29758  a12study10n  29759  hlhilslem  32753
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