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  mpto2  1524  mtp-xor  1525  mpgbir  1537  nfxfr  1557  19.35ri  1589  a9ev  1637  a9e  1891  cbval2  1944  cbvex2  1945  sbt  1973  moaneu  2202  moanmo  2203  axext2  2265  eqeltri  2353  nfcxfr  2416  neirr  2451  exmidne  2452  eqnetri  2463  mprgbir  2613  vex  2791  issetri  2795  moeq  2941  cdeqi  2976  ru  2990  eqsstri  3208  3sstr4i  3217  tpid1  3739  tpid2  3740  tpid3  3742  pwv  3826  uni0  3854  eqbrtri  4042  tr0  4124  trv  4125  zfrep4  4139  zfnuleu  4146  axnulALT  4147  0ex  4150  inex1  4155  0elpw  4180  axpow2  4190  axpow3  4191  pwex  4193  dvdemo1  4210  zfpair2  4215  exss  4236  moop2  4261  pwundif  4300  po0  4329  epse  4376  0elon  4445  nsuceq0  4472  uniex2  4515  snnex  4524  tfinds2  4654  finds  4682  finds2  4684  relsnop  4791  relxp  4794  rel0  4810  relopabi  4811  eliunxp  4823  opeliunxp2  4824  dmi  4893  xpidtr  5065  cnvcnv  5126  dmsn0  5140  cnvsn0  5141  funmpt  5290  funmpt2  5291  isarep2  5332  fresaunres2  5413  f0  5425  f10  5507  f1o00  5508  f1oi  5511  f1osn  5513  brprcneu  5518  fvopab3ig  5599  opabex  5744  eufnfv  5752  mpt2fun  5946  reldmmpt2  5955  oprabex  5961  oprabex3  5962  ovid  5964  ovidig  5965  ovidi  5966  ovig  5969  ov3  5984  caovmo  6057  relmptopab  6065  f1stres  6141  f2ndres  6142  relmpt2opab  6201  tpos0  6264  porpss  6281  opabiotafun  6291  canth  6294  ncanth  6295  issmo  6365  tfrlem6  6398  tfrlem8  6400  tfrlem16  6409  tfr1a  6410  tfr1  6413  tz7.44lem1  6418  seqomlem2  6463  seqomlem3  6464  seqomlem4  6465  fnseqom  6467  abianfp  6471  0lt1o  6503  0we1  6505  eqer  6693  ecopover  6762  th3qcor  6766  mapsnf1o3  6816  ssdomg  6907  ensn1  6925  snfi  6941  xpcomf1o  6951  map2xp  7031  limensuci  7037  sdom1  7062  unblem4  7112  fidomdm  7138  marypha1lem  7186  hartogslem1  7257  hartogs  7259  card2on  7268  ruv  7314  ruALT  7315  inf2  7324  inf3lem6  7334  infeq5i  7337  zfinf2  7343  cantnflt  7373  cantnf  7395  mapfien  7399  cnfcom  7403  trcl  7410  tz9.1c  7412  tc2  7427  r1funlim  7438  r1fnon  7439  karden  7565  tskwe  7583  cardprclem  7612  cardprc  7613  pm54.43  7633  r0weon  7640  iunmapdisj  7650  alephfnon  7692  alephfplem4  7734  alephfp  7735  alephval3  7737  aceq3lem  7747  kmlem2  7777  cda1dif  7802  ackbij1  7864  ackbij2lem2  7866  ackbij2  7869  infpssrlem3  7931  hsmexlem4  8055  hsmexlem5  8056  axdc3lem4  8079  ac2  8087  axac3  8090  ac6  8107  axdclem2  8147  ondomon  8185  alephsucpw  8192  pwcfsdom  8205  cfpwsdom  8206  smobeth  8208  axpowndlem3  8221  zfcndun  8237  zfcndpow  8238  zfcndinf  8240  zfcndac  8241  wunex2  8360  uniwun  8362  wuncid  8365  wuncval2  8369  grur1  8442  axgroth5  8446  axgroth2  8447  axgroth6  8450  axgroth3  8453  grothtsk  8457  inaprc  8458  ltsopi  8512  dmaddpi  8514  dmmulpi  8515  1lt2pi  8529  nqerf  8554  addnqf  8572  mulnqf  8573  1lt2nq  8597  0r  8702  1sr  8703  m1r  8704  m1p1sr  8714  m1m1sr  8715  0lt1sr  8717  axaddf  8767  axmulf  8768  ax1cn  8771  ax1ne0  8782  pnfnre  8874  mnfnre  8875  subaddrii  9135  ine0  9215  ixi  9397  recgt0ii  9662  nn1suc  9767  4d2e2  9876  nnunb  9961  arch  9962  un0mulcl  9998  nummac  10156  uzf  10233  indstr  10287  mnfltpnf  10465  ixxf  10666  ioof  10741  fzf  10786  fzp1disj  10843  fzof  10872  om2uzrani  11015  om2uzf1oi  11016  uzrdglem  11020  uzrdgfni  11021  uzrdg0i  11022  ltwenn  11025  hashgf1o  11033  axdc4uzlem  11044  sq0  11195  irec  11202  hashkf  11339  hashf  11344  hash0  11355  hashsslei  11378  hashxplem  11385  hashbclem  11390  hashf1lem1  11393  wrd0  11418  wrdexg  11425  revs1  11483  cats1fvn  11508  climmo  12031  fsumcom2  12237  ackbijnn  12286  incexclem  12295  infcvgaux1i  12315  efcvgfsum  12367  cos1bnd  12467  cos2bnd  12468  eirr  12483  znnen  12491  qnnen  12492  aleph1re  12523  sqr2irr  12527  nthruz  12530  dvdslelem  12573  3dvds  12591  divalglem5  12596  bitsf  12618  sadcaddlem  12648  sadadd2lem  12650  sadadd3  12652  sadaddlem  12657  isprm3  12767  2prm  12774  3prm  12775  phicl2  12836  pockthi  12954  unbenlem  12955  prmrec  12969  vdwlem13  13040  vdwnn  13045  ramcl2  13063  mod2xnegi  13086  modsubi  13087  structcnvcnv  13159  structfun  13160  setsres  13174  strfv  13180  strlemor1  13235  strleun  13238  0rest  13334  firest  13337  restid  13338  prdsval  13355  prdsbas  13357  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  prdsds  13363  imasaddfnlem  13430  imasvscafn  13439  oppchomfval  13617  oppcbas  13621  2oppchomf  13627  rescbas  13706  rescco  13709  rescabs  13710  idfucl  13755  wunnat  13830  homarel  13868  dmaf  13881  cdaf  13882  dmcoass  13898  catcfuccl  13941  xpcbas  13952  relxpchom  13955  catcxpccl  13981  oppchofcl  14034  oyoncl  14044  odubas  14237  letsr  14349  mgmidmo  14370  releqg  14664  ga0  14752  oppglem  14823  efgval  15026  efger  15027  efgsp1  15046  efgsfo  15048  efgredleme  15052  efgredlem  15056  efgred  15057  cygctb  15178  gsum2d2lem  15224  gsum2d2  15225  gsumcom2  15226  dprd2d2  15279  pgpfaclem1  15316  mgplem  15330  mgpress  15336  opprlem  15410  reldvdsr  15426  00lsp  15738  sralem  15930  srasca  15934  psrvscafval  16135  opsrbaslem  16219  psrbag0  16235  00ply1bas  16318  ply1plusgfvi  16320  zlmsca  16475  znbaslem  16492  ocvfval  16566  ocv0  16577  cssval  16582  thlbas  16596  thlle  16597  eltopspOLD  16656  tgdom  16716  tgidm  16718  indistps2ALT  16751  restbas  16889  resttopon  16892  rest0  16900  leordtval2  16942  iocpnfordt  16945  icomnfordt  16946  iooordt  16947  cnpfval  16964  iscnp2  16969  ist1-3  17077  1stcfb  17171  islly2  17210  1stckgen  17249  ptbasfi  17276  xkotf  17280  dfac14  17312  opnfbas  17537  zfbas  17591  hauspwpwf1  17682  alexsubALTlem4  17744  alexsubALT  17745  ptcmplem5  17750  0met  17930  prdsdsf  17931  prdsxmetlem  17932  prdsmet  17934  setsmsbas  18021  setsmsds  18022  prdsbl  18037  tngds  18164  qtopbaslem  18267  xrtgioo  18312  xrsdsre  18316  zcld  18319  recld2  18320  reperflem  18323  retopcon  18334  iccpnfcnv  18442  bndth  18456  ishtpy  18470  nmoleub2lem2  18597  recmet  18745  resscdrg  18775  ishl2  18787  volf  18888  iundisj2  18906  volsup  18913  icombl  18921  ioombl  18922  ismbf3d  19009  0plef  19027  0pledm  19028  itg1ge0  19041  mbfi1fseqlem5  19074  itg2addlem  19113  iblcnlem1  19142  reldv  19220  limciun  19244  dvexp  19302  dveflem  19326  lhop1lem  19360  lhop  19363  elply2  19578  elplyd  19584  ply1term  19586  ply0  19590  plymullem  19598  qaa  19703  aaliou3  19731  pserulm  19798  pserdvlem2  19804  efcn  19819  sincosq1lem  19865  tangtx  19873  sincos4thpi  19881  sincos6thpi  19883  pige3  19885  efif1olem4  19907  logf1o  19922  relogf1o  19924  log1  19939  loge  19940  relogiso  19951  dvrelog  19984  relogcn  19985  logcn  19994  cxpcn3  20088  resqrcn  20089  leibpi  20238  log2ublem1  20242  birthday  20249  emcllem5  20293  harmonicbnd  20297  harmonicbnd2  20298  emgt0  20300  harmonicbnd3  20301  ppiltx  20415  ppiublem1  20441  ppiub  20443  bclbnd  20519  bpos1lem  20521  bposlem8  20530  lgsquadlem2  20594  2sqlem9  20612  2sqlem10  20613  chebbnd1  20621  selberg2lem  20699  pntrsumo1  20714  selbergsb  20724  pntpbnd  20737  ex-dif  20810  ex-in  20812  ex-eprel  20820  ex-id  20821  ex-fl  20834  avril1  20836  2bornot2b  20837  grposn  20882  issubgoi  20977  0vfval  21162  vsfval  21191  ajmoi  21437  ajfuni  21438  normlem2  21690  norm3adifii  21727  hhip  21756  hlim0  21815  hlimcaui  21816  hlimf  21817  hhssnv  21841  shscli  21896  shsval2i  21966  h1de2i  22132  fh3i  22202  fh4i  22203  cm2mi  22205  qlaxr3i  22215  mayetes3i  22309  ho0f  22331  hoif  22334  hodidi  22367  ho0subi  22375  hosd1i  22402  adjmo  22412  nmopsetn0  22445  nmfnsetn0  22458  funadj  22466  funcnvadj  22473  nmcexi  22606  cnlnadjlem8  22654  nmoptri2i  22679  opsqrlem4  22723  hmopidmchi  22731  pjoci  22760  pjinvari  22771  rinvf1o  23038  ballotlem2  23047  ballotlemfc0  23051  ballotlemfcc  23052  ballotlem4  23057  ballotlemic  23065  ballotlem7  23094  ballotth  23096  elim2ifim  23153  abrexdomjm  23165  rabexgfGS  23171  pwundif2  23186  xpima  23202  xppreima2  23212  funcnvmptOLD  23234  funcnvmpt  23235  fzossnn  23278  xrge0iifcnv  23315  xrge0pluscn  23322  snct  23339  dmct  23342  iundisj2fi  23364  iundisj2f  23366  esumpcvgval  23446  hasheuni  23453  esumcvg  23454  dmvlsiga  23490  dmsigagen  23505  brsiga  23514  brsigarn  23515  measbasedom  23532  measvuni  23542  br2base  23574  coinflipprob  23680  coinfliprv  23683  coinflippvt  23685  subfacp1lem5  23715  subfacp1lem6  23716  kur14lem9  23745  cvmcov2  23806  cvmliftlem1  23816  cvmliftlem4  23819  cvmliftlem5  23820  umgra0  23877  umgrabi  23907  vdegp1ai  23908  vdegp1bi  23909  konigsberg  23911  ghomgrpilem2  23993  relexp0  24025  relexpsucr  24026  relexpsucl  24028  dfrtrclrec2  24040  rtrclreclem.refl  24041  rtrclreclem.subset  24042  rtrclreclem.min  24044  dfrtrcl2  24045  brtpid1  24075  brtpid2  24076  brtpid3  24077  domep  24149  axextndbi  24161  poseq  24253  wfrlem14  24269  wfrlem16  24271  frrlem10  24292  sltval2  24310  nosgnn0i  24313  brv  24417  txprel  24419  relsset  24428  relbigcup  24437  fvbigcup  24442  fnsingle  24458  fvsingle  24459  snelsingles  24461  funimage  24467  funpartfun  24481  fullfunfnv  24484  ax5seglem7  24563  axlowdimlem4  24573  axlowdimlem6  24575  axlowdimlem7  24576  axlowdimlem10  24579  axlowdimlem13  24582  axlowdimlem16  24585  axlowdimlem17  24586  axlowdim  24589  funtransport  24654  colinrel  24680  funray  24763  funline  24765  bpolylem  24783  bpoly3  24793  bpoly4  24794  0hf  24807  waj-ax  24853  lukshef-ax2  24854  arg-ax  24855  limsucncmpi  24884  vxveqv  25054  prj1b  25079  prj3  25080  inposet  25278  dominc  25280  rninc  25281  zintdom  25438  basexre  25522  intopcoaconlem3  25539  cntrset  25602  1ded  25738  relded  25740  reldded  25741  relrded  25742  relcat  25761  reldcat  25762  relrcat  25763  phckle  26027  psckle  26028  fnckle  26045  pfsubkl  26047  pvp  26048  pgapspf  26052  pgapspf2  26053  comppfsc  26307  neibastop2lem  26309  filnetlem3  26329  cover2  26358  abrexdom  26405  fdc  26455  cncfres  26485  heibor1lem  26533  moxfr  26752  mapfzcons1  26794  diophrw  26838  0dioph  26858  vdioph  26859  ftp  26893  rabren3dioph  26898  2nn0ind  27030  rpnnen3  27125  kelac2lem  27162  frlmpwfi  27262  islinds2  27283  psgnunilem3  27419  psgnunilem4  27420  matsca  27470  lhe4.4ex1a  27546  rusbcALT  27639  compneOLD  27643  ipo0  27652  ifr0  27653  rfcnpre1  27690  fnchoice  27700  rrpsscn  27719  dvcosre  27741  stoweidlem5  27754  stoweidlem13  27762  stoweidlem26  27775  stoweidlem28  27777  stoweidlem34  27783  stoweidlem44  27793  stoweidlem59  27808  stoweid  27812  wallispilem3  27816  wallispilem4  27817  wallispi2lem1  27820  stirlinglem5  27827  stirlinglem13  27835  stirlinglem14  27836  stirlingr  27839  usgra0  28116  usgra1v  28126  usgraex0elv  28128  usgraex1elv  28129  usgraex2elv  28130  usgraex3elv  28131  frgra0  28175  ex-gte  28199  AnelBC  28234  vk15.4j  28291  2sb5nd  28326  dfvd1ir  28341  dfvd2anir  28353  dfvd2ir  28355  dfvd3ir  28362  dfvd3anir  28365  iden2  28386  e0bir  28552  uun2221p1  28589  uun2221p2  28590  2sb5ndVD  28686  2sb5ndALT  28709  bnj226  28762  bnj1101  28816  bnj110  28890  bnj149  28907  bnj150  28908  bnj151  28909  bnj517  28917  bnj580  28945  bnj865  28955  bnj900  28961  bnj996  28987  bnj1110  29012  bnj1133  29019  bnj1128  29020  bnj1145  29023  bnj1137  29025  bnj1171  29030  bnj1176  29035  ax12conj2  29108  a12stdy1-x12  29111  a12study10  29136  a12study10n  29137  hlhilslem  32131
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