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  24220  axextndbi  24232  poseq  24324  wfrlem14  24340  wfrlem16  24342  frrlem10  24363  sltval2  24381  nosgnn0i  24384  brv  24488  txprel  24490  relsset  24499  relbigcup  24508  fvbigcup  24513  fnsingle  24529  fvsingle  24530  snelsingles  24532  funimage  24538  fullfunfnv  24556  ax5seglem7  24635  axlowdimlem4  24645  axlowdimlem6  24647  axlowdimlem7  24648  axlowdimlem10  24651  axlowdimlem13  24654  axlowdimlem16  24657  axlowdimlem17  24658  axlowdim  24661  funtransport  24726  colinrel  24752  funray  24835  funline  24837  bpolylem  24855  bpoly3  24865  bpoly4  24866  0hf  24879  waj-ax  24925  lukshef-ax2  24926  arg-ax  24927  limsucncmpi  24956  itg2addnc  25005  itgaddnclem2  25010  vxveqv  25157  prj1b  25182  prj3  25183  inposet  25381  dominc  25383  rninc  25384  zintdom  25541  basexre  25625  intopcoaconlem3  25642  cntrset  25705  1ded  25841  relded  25843  reldded  25844  relrded  25845  relcat  25864  reldcat  25865  relrcat  25866  phckle  26130  psckle  26131  fnckle  26148  pfsubkl  26150  pvp  26151  pgapspf  26155  pgapspf2  26156  comppfsc  26410  neibastop2lem  26412  filnetlem3  26432  cover2  26461  abrexdom  26508  fdc  26558  cncfres  26588  heibor1lem  26636  moxfr  26855  mapfzcons1  26897  diophrw  26941  0dioph  26961  vdioph  26962  ftp  26996  rabren3dioph  27001  2nn0ind  27133  rpnnen3  27228  kelac2lem  27265  frlmpwfi  27365  islinds2  27386  psgnunilem3  27522  psgnunilem4  27523  matsca  27573  lhe4.4ex1a  27649  rusbcALT  27742  compneOLD  27746  ipo0  27755  ifr0  27756  rfcnpre1  27793  fnchoice  27803  rrpsscn  27822  dvcosre  27844  stoweidlem5  27857  stoweidlem13  27865  stoweidlem26  27878  stoweidlem28  27880  stoweidlem34  27886  stoweidlem44  27896  stoweidlem59  27911  stoweid  27915  wallispilem3  27919  wallispilem4  27920  wallispi2lem1  27923  stirlinglem5  27930  stirlinglem13  27938  stirlinglem14  27939  stirlingr  27942  usgra0  28250  usgra1v  28260  usgraex0elv  28262  usgraex1elv  28263  usgraex2elv  28264  usgraex3elv  28265  0wlk  28343  0trl  28344  wlkntrllem2  28346  wlkntrllem3  28347  wlkntrllem4  28348  0pth  28356  usgrcyclnl2  28387  4cycl4dv  28413  frgra0  28421  ex-gte  28453  AnelBC  28488  vk15.4j  28590  2sb5nd  28625  dfvd1ir  28640  dfvd2anir  28652  dfvd2ir  28654  dfvd3ir  28661  dfvd3anir  28664  iden2  28691  e0bir  28866  uun2221p1  28903  uun2221p2  28904  2sb5ndVD  29002  2sb5ndALT  29025  bnj226  29078  bnj1101  29132  bnj110  29206  bnj149  29223  bnj150  29224  bnj151  29225  bnj517  29233  bnj580  29261  bnj865  29271  bnj900  29277  bnj996  29303  bnj1110  29328  bnj1133  29335  bnj1128  29336  bnj1145  29339  bnj1137  29341  bnj1171  29346  bnj1176  29351  a9eNEW7  29447  sbtNEW7  29603  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