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

Theorem mpbir 214
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992.)
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 211 . 2  |-  ( ps 
->  ph )
41, 3ax-mp 5 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 190
This theorem is referenced by:  pm5.74ri  254  con4bii  303  orri  382  imorri  420  imnani  429  mpbir2an  931  mpbir3an  1191  xorexmid  1427  tru  1452  had1  1510  nic-mpALT  1559  nic-ax  1560  nic-axALT  1561  mpgbir  1677  nfxfr  1700  19.35ri  1746  ax5e  1764  ax6ev  1811  exan  2058  ax13  2142  euequ1  2306  moanmo  2362  axi12  2430  axext2  2433  eqeltri  2526  nfcxfr  2591  neir  2627  neirr  2633  eqnetri  2694  nelir  2727  mprgbir  2752  vex  3016  issetri  3020  moeq  3182  rmoeq  3205  cdeqi  3220  eqsstri  3430  3sstr4i  3439  rabrsn  4011  tpid1  4054  tpid2  4055  tpid3  4057  pwv  4167  uni0  4195  eqbrtri  4394  tr0  4480  trv  4481  zfrep4  4495  zfnuleu  4502  axnulALT  4503  0ex  4507  inex1  4516  0elpw  4545  axpow2  4556  axpow3  4557  pwex  4559  dvdemo1  4608  zfpair2  4613  exss  4636  moop2  4669  pwundif  4719  po0  4748  epse  4795  relsnop  4917  relxp  4920  rel0  4936  relopabi  4937  eliunxp  4950  opeliunxp2  4951  dmi  5027  xpidtr  5200  xpima  5257  cnvcnv  5267  dmsn0  5282  cnvsn0  5283  0elon  5455  funmpt  5597  funmpt2  5598  funcnv0  5622  isarep2  5645  fresaunres2  5738  f0  5747  f10  5828  f10d  5829  f1o00  5830  f1oi  5833  f1osn  5835  brprcneu  5841  opabiotafun  5910  fvopab3ig  5929  opabex  6120  eufnfv  6125  canth  6235  ncanth  6236  mpt2fun  6386  reldmmpt2  6395  ovid  6401  ovidig  6402  ovidi  6403  ovig  6406  ov3  6421  caovmo  6494  relmptopab  6505  porpss  6563  uniex2  6574  snnex  6585  tfinds2  6678  finds  6707  finds2  6709  oprabex  6769  oprabex3  6770  f1stres  6803  f2ndres  6804  relmpt2opab  6866  opeliunxp2f  6944  tpos0  6990  wfrrel  7028  wfrlem14  7036  wfrlem16  7038  issmo  7054  tfrlem6  7087  tfrlem8  7089  tfrlem16  7098  tfr1a  7099  tfr1  7102  tz7.44lem1  7110  seqomlem2  7155  seqomlem3  7156  seqomlem4  7157  fnseqom  7159  0lt1o  7193  0we1  7195  eqer  7383  ecopover  7454  mapsnf1o3  7507  ssdomg  7602  ensn1  7620  snfi  7637  xpcomf1o  7648  map2xp  7729  limensuci  7735  sdom1  7759  unblem4  7813  fidomdm  7840  marypha1lem  7934  hartogslem1  8044  hartogs  8046  card2on  8056  ruALT  8103  inf2  8115  inf3lem6  8125  infeq5i  8128  zfinf2  8134  cantnflt  8164  cnfcom  8192  trcl  8199  tz9.1c  8201  tc2  8213  r1funlim  8224  r1fnon  8225  karden  8353  tskwe  8371  cardprclem  8400  pm54.43  8421  r0weon  8430  iunmapdisj  8441  alephfnon  8483  alephfplem4  8525  alephfp  8526  alephval3  8528  aceq3lem  8538  kmlem2  8568  cda1dif  8593  ackbij1  8655  ackbij2lem2  8657  ackbij2  8660  infpssrlem3  8722  hsmexlem4  8846  hsmexlem5  8847  axdc3lem4  8870  ac2  8878  axac3  8881  ac6  8897  axdclem2  8937  ondomon  8975  alephsucpw  8982  pwcfsdom  8995  cfpwsdom  8996  smobeth  8998  axpowndlem3  9011  zfcndun  9027  zfcndpow  9028  zfcndinf  9030  zfcndac  9031  wunex2  9150  uniwun  9152  wuncval2  9159  grur1  9232  axgroth5  9236  axgroth2  9237  axgroth6  9240  axgroth3  9243  grothtsk  9247  inaprc  9248  ltsopi  9300  dmaddpi  9302  dmmulpi  9303  1lt2pi  9317  nqerf  9342  addnqf  9360  mulnqf  9361  1lt2nq  9385  m1p1sr  9503  m1m1sr  9504  0lt1sr  9506  axaddf  9556  axmulf  9557  ax1cn  9560  subaddrii  9951  ixi  10230  recgt0ii  10501  nn1suc  10619  neg1lt0  10705  4d2e2  10756  arch  10856  un0mulcl  10894  nummac  11073  uzf  11152  indstr  11217  mnfltpnf  11418  ixxf  11635  ioof  11722  fzf  11779  0nelfz1  11809  fzp1disj  11845  fzp1nel  11869  fzof  11910  om2uzrani  12160  om2uzf1oi  12161  uzrdglem  12165  uzrdgfni  12166  uzrdg0i  12167  ltwenn  12170  hashgf1o  12178  axdc4uzlem  12189  sq0  12360  irec  12368  facmapnn  12464  hashkf  12511  hashf  12516  hash0  12542  prhash2ex  12570  hashsslei  12593  hashxplem  12600  hashbclem  12610  hashf1lem1  12613  wrdexg  12677  wrd0OLD  12690  s1dm  12744  revs1  12869  0csh0  12894  cshw1  12920  cats1fvn  12953  s2dm  12983  funcnvs1  13005  relexp0g  13096  relexpsucnnr  13099  dfrtrclrec2  13131  rtrclreclem1  13132  rtrclreclem2  13133  rtrclreclem4  13135  dfrtrcl2  13136  climmo  13632  fsumcom2  13846  ackbijnn  13897  incexclem  13905  infcvgaux1i  13926  fprodcom2  14049  fprodn0f  14056  fprodge0  14058  fprodge1  14060  bpolylem  14112  bpoly3  14122  bpoly4  14123  efcvgfsum  14151  cos1bnd  14252  cos2bnd  14253  znnen  14276  qnnen  14277  aleph1re  14308  3dvds  14380  divalglem5OLD  14387  divalglem5  14388  bitsf  14411  sadcaddlem  14442  sadadd2lem  14444  sadadd3  14446  sadaddlem  14451  lcmf0  14618  lcmfunsnlem2lem1  14622  lcmfunsnlem2  14624  2prm  14651  coprmprod  14689  coprmproddvdslem  14690  3lcm2e6  14692  phicl2  14727  pockthi  14862  unbenlem  14863  prmrec  14877  vdwlem13  14954  vdwnn  14959  ramcl2  14984  ramcl2OLD  14985  lcmsmapnnOLD  15022  prmormapnnOLD  15025  prmgapprmo  15044  mod2xnegi  15054  modsubi  15055  prmo4  15110  prmo5  15111  prmo6  15112  structcnvcnv  15143  structfun  15144  setsres  15162  strfv  15168  strlemor1  15228  strleun  15231  0rest  15339  firest  15342  restid  15343  prdsval  15364  prdsbas  15366  prdsplusg  15367  prdsmulr  15368  prdsvsca  15369  prdsds  15373  imasaddfnlem  15445  imasvscafn  15454  oppchomfval  15630  oppcbas  15634  2oppchomf  15640  rescbas  15745  rescco  15748  rescabs  15749  0ssc  15753  0subcat  15754  idfucl  15797  wunnat  15872  homarel  15942  dmaf  15955  cdaf  15956  catcfuccl  16015  relxpchom  16077  catcxpccl  16103  oppchofcl  16156  oyoncl  16166  odubas  16390  letsr  16484  mgmidmo  16513  releqg  16875  ga0  16963  oppglem  17012  psgnunilem3  17148  psgnunilem4  17149  pmtrsn  17171  efgval  17378  efger  17379  efgsp1  17398  efgsfo  17400  efgredleme  17404  efgredlem  17408  efgred  17409  cygctb  17537  gsum2d2lem  17616  gsum2d2  17617  gsumcom2  17618  dprd2d2  17688  pgpfaclem1  17725  mgplem  17739  mgpress  17745  opprlem  17867  reldvdsr  17883  00lsp  18215  sralem  18411  srasca  18415  sravsca  18416  psrvscafval  18625  opsrbaslem  18712  psrbag0  18728  00ply1bas  18844  ply1plusgfvi  18846  xrsmgm  19014  zlmsca  19103  znbaslem  19120  resubdrg  19187  ocvfval  19240  ocv0  19251  cssval  19256  thlbas  19270  thlle  19271  islinds2  19382  matsca  19451  m2detleib  19667  tgdom  20005  tgidm  20007  indistps2ALT  20040  restbas  20185  resttopon  20188  rest0  20196  leordtval2  20239  iocpnfordt  20242  icomnfordt  20243  iooordt  20244  cnpfval  20261  iscnp2  20266  ist1-3  20376  1stcfb  20471  islly2  20510  comppfsc  20558  1stckgen  20580  ptbasfi  20607  xkotf  20611  dfac14  20644  opnfbas  20868  hauspwpwf1  21013  alexsubALTlem4  21076  alexsubALT  21077  ptcmplem5  21082  cnextrel  21089  ust0  21245  tuslem  21293  0met  21392  prdsdsf  21393  prdsxmetlem  21394  prdsmet  21396  setsmsbas  21501  setsmsds  21502  prdsbl  21517  tngds  21667  qtopbaslem  21790  xrtgioo  21835  xrsdsre  21839  zcld  21842  recld2  21843  sszcld  21846  reperflem  21847  retopcon  21858  iccpnfcnv  21983  bndth  21997  ishtpy  22014  nmoleub2lem2  22141  recmet  22302  resscdrg  22336  ishl2  22348  recms  22350  volf  22494  iundisj2  22514  volsup  22521  icombl  22529  ioombl  22530  ismbf3d  22622  0plef  22642  0pledm  22643  itg1ge0  22656  mbfi1fseqlem5  22689  itg2addlem  22728  iblcnlem1  22757  reldv  22837  limciun  22861  dvexp  22919  dveflem  22943  lhop1lem  22977  lhop  22980  elply2  23162  elplyd  23168  ply1term  23170  ply0  23174  plymullem  23182  qaa  23291  pserulm  23389  pserdvlem2  23395  efcn  23410  sincosq1lem  23464  tangtx  23472  sincos4thpi  23480  sincos6thpi  23482  pige3  23484  efif1olem4  23506  logf1o  23526  relogf1o  23528  log1  23547  loge  23548  relogiso  23559  dvrelog  23594  relogcn  23595  logcn  23604  cxpcn3  23700  resqrtcn  23701  leibpi  23880  log2ublem1  23884  birthday  23892  emcllem5  23937  harmonicbnd  23941  harmonicbnd2  23942  emgt0  23944  harmonicbnd3  23945  lgamgulm2  23973  lgamcvglem  23977  gamf  23980  ppiltx  24116  ppiublem1  24142  ppiub  24144  bclbnd  24220  bpos1lem  24222  bposlem8  24231  lgsquadlem2  24295  2sqlem9  24313  2sqlem10  24314  chebbnd1  24322  selberg2lem  24400  pntrsumo1  24415  selbergsb  24425  pntpbnd  24438  istrkg2ld  24520  tgcgr4  24588  ttgval  24917  ttglem  24918  cchhllem  24929  ax5seglem7  24977  axlowdimlem4  24987  axlowdimlem6  24989  axlowdimlem7  24990  axlowdimlem10  24993  axlowdimlem13  24996  axlowdimlem16  24999  uhgra0  25048  umgra0  25064  usgra1v  25129  cusgraexilem2  25207  cusgrasizeindslem2  25214  0wlk  25287  0trl  25288  wlkntrllem2  25302  wlkntrl  25304  0pth  25312  1pthonlem1  25331  usgrcyclnl2  25381  4cycl4dv  25407  wwlknext  25464  wwlknfi  25478  disjxwwlkn  25485  vdgrf  25638  umgrabi  25723  vdegp1ai  25724  vdegp1bi  25725  konigsberg  25727  frgra0  25734  numclwwlkdisj  25820  numclwwlk3lem  25848  ex-dif  25885  ex-in  25887  ex-eprel  25895  ex-id  25896  ex-fl  25909  avril1  25912  2bornot2b  25913  grposn  25955  issubgoi  26050  0vfval  26237  vsfval  26266  ajmoi  26512  ajfuni  26513  normlem2  26776  norm3adifii  26813  hhip  26842  hlim0  26900  hlimcaui  26901  hlimf  26902  hhssnv  26927  shscli  26982  shsval2i  27052  h1de2i  27218  fh3i  27288  fh4i  27289  cm2mi  27291  qlaxr3i  27301  mayetes3i  27394  ho0f  27416  hoif  27419  hodidi  27452  ho0subi  27460  hosd1i  27487  adjmo  27497  nmopsetn0  27530  nmfnsetn0  27543  funadj  27551  funcnvadj  27558  nmcexi  27691  cnlnadjlem8  27739  nmoptri2i  27764  opsqrlem4  27808  hmopidmchi  27816  pjoci  27845  pjinvari  27856  abrexdomjm  28153  elim2ifim  28173  iundisj2f  28210  mptexgf  28234  rinvf1o  28239  funcnvmptOLD  28278  dfcnv2  28287  snct  28303  dmct  28306  fpwrelmap  28326  iundisj2fi  28381  gsumle  28549  xrge0slmod  28614  xrge0pluscn  28753  zlmds  28775  zlmtset  28776  qqhre  28831  esumrnmpt2  28896  esumfsup  28898  esumpcvgval  28906  hasheuni  28913  esumcvg  28914  esumcvgsum  28916  esumsup  28917  esum2d  28921  dmsigagen  28973  ldgenpisyslem3  28994  measvuni  29043  voliune  29058  volfiniune  29059  br2base  29097  dya2iocuni  29111  eulerpartlem1  29206  eulerpartlemt  29210  eulerpartgbij  29211  fib0  29238  coinfliprv  29321  ballotlem2  29327  ballotlemic  29345  ballotlem7  29374  ballotth  29376  ballotlemicOLD  29383  ballotlem7OLD  29412  ballotthOLD  29414  plymul02  29441  bnj226  29548  bnj1101  29602  bnj110  29675  bnj149  29692  bnj150  29693  bnj151  29694  bnj517  29702  bnj580  29730  bnj865  29740  bnj900  29746  bnj996  29772  bnj1110  29797  bnj1133  29804  bnj1128  29805  bnj1145  29808  bnj1137  29810  bnj1171  29815  bnj1176  29820  subfacp1lem5  29913  subfacp1lem6  29914  kur14lem9  29943  cvmcov2  30004  cvmliftlem1  30014  cvmliftlem4  30017  cvmliftlem5  30018  msrfo  30190  problem5  30307  ghomgrpilem2  30310  brtpid1  30359  brtpid2  30360  brtpid3  30361  logi  30376  faclimlem1  30385  domep  30445  axextndbi  30457  poseq  30497  frrlem10  30531  sltval2  30549  brv  30650  txprel  30652  relsset  30661  relbigcup  30670  fvbigcup  30675  fnsingle  30692  fvsingle  30693  snelsingles  30695  funimage  30701  fullfunfnv  30719  imagesset  30726  funtransport  30804  colinrel  30830  funray  30913  funline  30915  0hf  30950  neibastop2lem  31022  filnetlem3  31042  waj-ax  31080  lukshef-ax2  31081  arg-ax  31082  limsucncmpi  31111  bj-babylob  31190  bj-nalnalimiOLD  31225  bj-nfv  31232  bj-ax12ssb  31250  bj-dvdemo1  31419  bj-disjcsn  31544  bj-snsetex  31559  bj-0eltag  31574  bj-2upln0  31619  bj-2upln1upl  31620  f1omptsnlem  31740  f1omptsn  31741  icoreresf  31757  relowlssretop  31768  relowlpssretop  31769  pigt3  31940  poimirlem3  31945  poimirlem9  31951  poimirlem16  31958  poimirlem17  31959  poimirlem18  31960  poimirlem19  31961  poimirlem20  31962  poimirlem26  31968  mblfinlem1  31979  mblfinlem2  31980  ismblfin  31983  voliunnfl  31986  cnambfre  31991  dvtanlemOLD  31993  cover2  32042  abrexdom  32059  fdc  32076  cncfres  32099  heibor1lem  32143  bicontr  32315  an12i  32336  tsim1  32374  ac6s6f  32418  elimhyps  32535  dedths  32536  renegclALT  32537  hlhilslem  35511  moxfr  35536  mapfzcons1  35561  diophrw  35603  0dioph  35623  vdioph  35624  rabren3dioph  35660  2nn0ind  35795  rpnnen3  35889  kelac2lem  35924  frlmpwfi  35958  ifpbiidcor2  36129  relintabex  36189  eliunov2  36273  xphe  36378  xpheOLD  36379  0he  36380  he0  36382  snhesn  36384  idhe  36385  frege54cor1c  36513  amgm2d  36651  amgm3d  36652  amgm4d  36653  lhe4.4ex1a  36679  rusbcALT  36791  ipo0  36803  ifr0  36804  vk15.4j  36886  2sb5nd  36928  dfvd1ir  36943  dfvd2anir  36954  dfvd2ir  36956  dfvd3ir  36963  dfvd3anir  36966  iden2  36993  e0bir  37161  uun2221p1  37198  uun2221p2  37199  2sb5ndVD  37304  2sb5ndALT  37326  iunconlem2  37329  fnchoice  37347  elini  37375  unisn0  37389  elpwi2  37438  icof  37513  fsumiunss  37695  resincncf  37794  dvnprodlem3  37865  mbf0  37876  volioc  37891  volico  37903  dmvolss  37905  volioof  37907  stoweidlem13  37930  stoweidlem34  37952  stirlinglem5  37997  stirlinglem13  38005  stirlingr  38009  fourierdlem42  38069  fourierdlem42OLD  38070  fourierdlem62  38089  fouriersw  38152  etransc  38206  salexct  38250  salexct2  38255  salgencntex  38259  sge0rnn0  38269  gsumge0cl  38272  sge00  38277  sge0resplit  38307  omeiunle  38402  0ome  38414  icoresmbl  38428  ovn0lem  38450  ovnhoilem1  38486  hspmbl  38514  ovolval5lem3  38539  aistia  38575  aisfina  38576  aiffnbandciffatnotciffb  38582  axorbciffatcxorb  38583  abnotbtaxb  38594  abnotataxb  38595  0noddALTV  38909  2noddALTV  38913  nnsum3primes4  38974  evengpop3  38984  pfx2  39046  pnf0xnn0  39176  uhgr0e  39263  uhgr0  39265  usgr0  39420  usgrexmpllem  39434  usgrexmpl  39437  griedg0prc  39438  uvtxupgrres  39583  cplgr0  39595  usgrexi  39608  rgrusgrprc  39706  rusgrprc  39707  rgrprcx  39709  rgrx0ndm  39710  pthdlem2  39846  uspgrn2crct  39878  0ewlk  39880  01wlk  39884  0pth-av  39893  1pthdlem1  39902  1trld  39909  1wlk2v2elem2  39923  1wlk2v2e  39924  upgr3v3e3cycl  39973  upgr4cycl4dv4e  39978  dfconngr1  39981  0conngr  39985  usgra2pthspth  39990  usgra2pthlem1  39992  uhg0e  40013  oddinmgm  40140  2zrngamgm  40264  2zrngaabl  40269  2zrngmmgm  40271  2zrngnring  40277  fldhmsubc  40411  fldhmsubcALTV  40430  eliunxp2  40440  zlmodzxzldeplem  40616  zlmodzxzldep  40622  ldepslinc  40627  3halfnz  40642  ex-gte  40774  empty-surprise  40846  eximp-surprise2  40849
  Copyright terms: Public domain W3C validator