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

Theorem mpbir 202
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbir.min
mpbir.maj
Assertion
Ref Expression
mpbir

Proof of Theorem mpbir
StepHypRef Expression
1 mpbir.min . 2
2 mpbir.maj . . 3
32biimpri 199 . 2
41, 3ax-mp 5 1
Colors of variables: wff set class
Syntax hints:  <->wb 178
This theorem is referenced by:  pm5.74ri  239  con4bii  290  orri  367  imorri  405  imnani  414  mpbir2an  888  mpbir3an  1144  tru  1339  nic-mpALT  1456  nic-ax  1457  nic-axALT  1458  mtp-xor  1554  mpgbir  1566  nfxfr  1586  19.35ri  1622  a6ev  1679  exan  1899  cbval2OLD  1989  cbvex2  1990  ax13  2017  a6eOLD  2031  sbtOLD  2128  moanmo  2380  moaneuOLD  2382  axi12  2460  axext2  2463  eqeltri  2551  nfcxfr  2614  neir  2649  neirr  2651  exmidne  2652  eqnetri  2663  nesymir  2687  nelir  2744  mprgbir  2822  vex  3009  issetri  3013  moeq  3161  cdeqi  3197  eqsstri  3411  3sstr4i  3420  tpid1  4002  tpid2  4003  tpid3  4005  pwv  4100  uni0  4128  eqbrtri  4321  tr0  4406  trv  4407  zfrep4  4421  zfnuleu  4428  axnulALT  4429  0ex  4432  inex1  4443  0elpw  4468  axpow2  4479  axpow3  4480  pwex  4482  dvdemo1  4534  zfpair2  4539  exss  4562  moop2  4590  pwundif  4631  po0  4659  epse  4706  0elon  4775  relsnop  4948  relxp  4951  rel0  4968  relopabi  4969  eliunxp  4981  opeliunxp2  4982  dmi  5058  xpidtr  5222  xpima  5280  cnvcnv  5289  dmsn0  5305  cnvsn0  5306  funmpt  5453  funmpt2  5454  isarep2  5495  fresaunres2  5579  f0  5588  f10  5666  f1o00  5667  f1oi  5670  f1osn  5672  brprcneu  5678  opabiotafun  5745  fvopab3ig  5764  opabex  5925  eufnfv  5929  canth  6023  ncanth  6024  mpt2fun  6161  reldmmpt2  6170  ovid  6175  ovidig  6176  ovidi  6177  ovig  6180  ov3  6195  caovmo  6267  relmptopab  6275  porpss  6330  uniex2  6341  snnex  6348  tfinds2  6439  finds  6467  finds2  6469  oprabex  6526  oprabex3  6527  f1stres  6559  f2ndres  6560  relmpt2opab  6612  tpos0  6692  issmo  6722  tfrlem6  6755  tfrlem8  6757  tfrlem16  6766  tfr1a  6767  tfr1  6770  tz7.44lem1  6775  seqomlem2  6820  seqomlem3  6821  seqomlem4  6822  fnseqom  6824  abianfp  6828  0lt1o  6860  0we1  6862  eqer  7050  ecopover  7120  th3qcor  7124  mapsnf1o3  7174  ssdomg  7265  ensn1  7283  snfi  7299  xpcomf1o  7309  map2xp  7389  limensuci  7395  sdom1  7420  unblem4  7474  fidomdm  7500  marypha1lem  7550  hartogslem1  7623  hartogs  7625  card2on  7634  ruALT  7681  inf2  7690  inf3lem6  7700  infeq5i  7703  zfinf2  7709  cantnflt  7739  cantnf  7761  mapfien  7765  cnfcom  7769  trcl  7776  tz9.1c  7778  tc2  7793  r1funlim  7804  r1fnon  7805  karden  7933  tskwe  7951  cardprclem  7980  pm54.43  8001  r0weon  8008  iunmapdisj  8018  alephfnon  8060  alephfplem4  8102  alephfp  8103  alephval3  8105  aceq3lem  8115  kmlem2  8145  cda1dif  8170  ackbij1  8232  ackbij2lem2  8234  ackbij2  8237  infpssrlem3  8299  hsmexlem4  8423  hsmexlem5  8424  axdc3lem4  8447  ac2  8455  axac3  8458  ac6  8474  axdclem2  8514  ondomon  8552  alephsucpw  8559  pwcfsdom  8572  cfpwsdom  8573  smobeth  8575  axpowndlem3  8588  zfcndun  8604  zfcndpow  8605  zfcndinf  8607  zfcndac  8608  wunex2  8727  uniwun  8729  wuncval2  8736  grur1  8809  axgroth5  8813  axgroth2  8814  axgroth6  8817  axgroth3  8820  grothtsk  8824  inaprc  8825  ltsopi  8879  dmaddpi  8881  dmmulpi  8882  1lt2pi  8896  nqerf  8921  addnqf  8939  mulnqf  8940  1lt2nq  8964  m1p1sr  9081  m1m1sr  9082  0lt1sr  9084  axaddf  9134  axmulf  9135  ax1cn  9138  subaddrii  9515  ixi  9781  recgt0ii  10047  nn1suc  10152  neg1lt0  10237  4d2e2  10287  arch  10385  un0mulcl  10423  nummac  10594  uzf  10671  indstr  10730  mnfltpnf  10913  ixxf  11117  ioof  11193  fzf  11240  fzp1disj  11311  fzof  11345  om2uzrani  11567  om2uzf1oi  11568  uzrdglem  11572  uzrdgfni  11573  uzrdg0i  11574  ltwenn  11577  hashgf1o  11585  axdc4uzlem  11596  sq0  11749  irec  11757  hashkf  11897  hashf  11902  hash0  11927  hashsslei  11968  hashxplem  11982  hashbclem  11992  hashf1lem1  11995  wrdexg  12031  wrd0  12039  revs1  12191  0csh0  12216  cshw1  12242  cats1fvn  12271  climmo  12821  fsumcom2  13028  ackbijnn  13077  incexclem  13085  infcvgaux1i  13105  efcvgfsum  13157  cos1bnd  13257  cos2bnd  13258  znnen  13281  qnnen  13282  aleph1re  13313  dvdslelem  13363  3dvds  13382  divalglem5  13387  bitsf  13409  sadcaddlem  13439  sadadd2lem  13441  sadadd3  13443  sadaddlem  13448  isprm3  13558  2prm  13565  phicl2  13629  pockthi  13754  unbenlem  13755  prmrec  13769  vdwlem13  13840  vdwnn  13845  ramcl2  13863  mod2xnegi  13886  modsubi  13887  structcnvcnv  13971  structfun  13972  setsres  13986  strfv  13992  strlemor1  14047  strleun  14050  0rest  14148  firest  14151  restid  14152  prdsval  14169  prdsbas  14171  prdsplusg  14172  prdsmulr  14173  prdsvsca  14174  prdsds  14177  imasaddfnlem  14244  imasvscafn  14253  oppchomfval  14431  oppcbas  14435  2oppchomf  14441  rescbas  14520  rescco  14523  rescabs  14524  idfucl  14569  wunnat  14644  homarel  14682  dmaf  14695  cdaf  14696  catcfuccl  14755  relxpchom  14769  catcxpccl  14795  oppchofcl  14848  oyoncl  14858  odubas  15081  letsr  15175  mgmidmo  15196  releqg  15490  ga0  15578  oppglem  15649  efgval  15852  efger  15853  efgsp1  15872  efgsfo  15874  efgredleme  15878  efgredlem  15882  efgred  15883  cygctb  16004  gsum2d2lem  16050  gsum2d2  16051  gsumcom2  16052  dprd2d2  16105  pgpfaclem1  16142  mgplem  16156  mgpress  16162  opprlem  16236  reldvdsr  16252  00lsp  16560  sralem  16752  srasca  16756  psrvscafval  16957  opsrbaslem  17041  psrbag0  17057  00ply1bas  17137  ply1plusgfvi  17139  zlmsca  17305  znbaslem  17322  ocvfval  17396  ocv0  17407  cssval  17412  thlbas  17426  thlle  17427  eltopspOLD  17486  tgdom  17546  tgidm  17548  indistps2ALT  17581  restbas  17725  resttopon  17728  rest0  17736  leordtval2  17779  iocpnfordt  17782  icomnfordt  17783  iooordt  17784  cnpfval  17801  iscnp2  17806  ist1-3  17916  1stcfb  18012  islly2  18051  1stckgen  18090  ptbasfi  18117  xkotf  18121  dfac14  18154  opnfbas  18378  hauspwpwf1  18523  alexsubALTlem4  18585  alexsubALT  18586  ptcmplem5  18591  cnextrel  18598  ust0  18753  tuslem  18801  0met  18900  prdsdsf  18901  prdsxmetlem  18902  prdsmet  18904  setsmsbas  19009  setsmsds  19010  prdsbl  19025  tngds  19193  qtopbaslem  19296  xrtgioo  19341  xrsdsre  19345  zcld  19348  recld2  19349  sszcld  19352  reperflem  19353  retopcon  19364  iccpnfcnv  19473  bndth  19487  ishtpy  19501  nmoleub2lem2  19628  recmet  19780  resscdrg  19816  ishl2  19828  volf  19929  iundisj2  19947  volsup  19954  icombl  19962  ioombl  19963  ismbf3d  20048  0plef  20066  0pledm  20067  itg1ge0  20080  mbfi1fseqlem5  20113  itg2addlem  20152  iblcnlem1  20181  reldv  20261  limciun  20285  dvexp  20343  dveflem  20367  lhop1lem  20401  lhop  20404  elply2  20619  elplyd  20625  ply1term  20627  ply0  20631  plymullem  20639  qaa  20744  pserulm  20842  pserdvlem2  20848  efcn  20863  sincosq1lem  20914  tangtx  20922  sincos4thpi  20930  sincos6thpi  20932  pige3  20934  efif1olem4  20956  logf1o  20971  relogf1o  20973  log1  20989  loge  20990  relogiso  21001  dvrelog  21037  relogcn  21038  logcn  21047  cxpcn3  21141  resqrcn  21142  leibpi  21291  log2ublem1  21295  birthday  21302  emcllem5  21347  harmonicbnd  21351  harmonicbnd2  21352  emgt0  21354  harmonicbnd3  21355  ppiltx  21469  ppiublem1  21495  ppiub  21497  bclbnd  21573  bpos1lem  21575  bposlem8  21584  lgsquadlem2  21648  2sqlem9  21666  2sqlem10  21667  chebbnd1  21675  selberg2lem  21753  pntrsumo1  21768  selbergsb  21778  pntpbnd  21791  uhgra0  21853  umgra0  21869  usgra0  21899  usgra1v  21918  cusgraexilem2  21985  cusgrasizeindslem2  21992  0wlk  22054  0trl  22055  wlkntrllem2  22069  wlkntrl  22071  0pth  22079  1pthonlem1  22098  usgrcyclnl2  22137  4cycl4dv  22163  vdgrf  22178  umgrabi  22214  vdegp1ai  22215  vdegp1bi  22216  konigsberg  22218  ex-dif  22240  ex-in  22242  ex-eprel  22250  ex-id  22251  ex-fl  22264  avril1  22266  2bornot2b  22267  grposn  22312  issubgoi  22407  0vfval  22594  vsfval  22623  ajmoi  22869  ajfuni  22870  normlem2  23123  norm3adifii  23160  hhip  23189  hlim0  23248  hlimcaui  23249  hlimf  23250  hhssnv  23275  shscli  23330  shsval2i  23400  h1de2i  23566  fh3i  23636  fh4i  23637  cm2mi  23639  qlaxr3i  23649  mayetes3i  23743  ho0f  23765  hoif  23768  hodidi  23801  ho0subi  23809  hosd1i  23836  adjmo  23846  nmopsetn0  23879  nmfnsetn0  23892  funadj  23900  funcnvadj  23907  nmcexi  24040  cnlnadjlem8  24088  nmoptri2i  24113  opsqrlem4  24157  hmopidmchi  24165  pjoci  24194  pjinvari  24205  abrexdomjm  24504  elim2ifim  24526  iundisj2f  24551  rinvf1o  24569  funcnvmptOLD  24607  dfcnv2  24615  snct  24632  dmct  24635  fpwrelmap  24654  iundisj2fi  24702  nn0srg  24862  rge0srg  24863  gsumle  24897  reofld  24978  rearchi  24980  xrge0slmod  24982  xrge0iifcnv  25033  xrge0pluscn  25040  recms  25059  zlmds  25064  zlmtset  25065  cnzh  25070  rezh  25071  qqhre  25117  esumfsup  25190  esumpcvgval  25198  hasheuni  25205  esumcvg  25206  dmsigagen  25258  measvuni  25299  voliune  25316  volfiniune  25317  ddemeas  25323  br2base  25355  dya2iocuni  25369  eulerpartlem1  25415  eulerpartlemt  25419  eulerpartgbij  25420  eulerpartlemgh  25426  coinfliprv  25506  ballotlem2  25512  ballotlemfc0  25516  ballotlemfcc  25517  ballotlemic  25530  ballotlem7  25559  ballotth  25561  plymul02  25589  signswmnd  25600  lgamgulm2  25659  lgamcvglem  25663  gamf  25666  subfacp1lem5  25709  subfacp1lem6  25710  kur14lem9  25739  cvmcov2  25801  cvmliftlem1  25811  cvmliftlem4  25814  cvmliftlem5  25815  ghomgrpilem2  25936  relexp0  25962  relexpsucr  25963  relexpsucl  25965  dfrtrclrec2  25976  rtrclreclem.refl  25977  rtrclreclem.subset  25978  rtrclreclem.min  25980  dfrtrcl2  25981  brtpid1  26008  brtpid2  26009  brtpid3  26010  fzp1nel  26040  fprodcom2  26138  faclimlem1  26192  domep  26250  axextndbi  26262  poseq  26358  wfrlem6  26373  wfrlem14  26381  wfrlem16  26383  frrlem10  26423  sltval2  26441  nosgnn0i  26444  brv  26552  txprel  26554  relsset  26563  relbigcup  26572  fvbigcup  26577  fnsingle  26594  fvsingle  26595  snelsingles  26597  funimage  26603  fullfunfnv  26621  imagesset  26628  ax5seglem7  26704  axlowdimlem4  26714  axlowdimlem6  26716  axlowdimlem7  26717  axlowdimlem10  26720  axlowdimlem13  26723  axlowdimlem16  26726  axlowdimlem17  26727  axlowdim  26730  funtransport  26795  colinrel  26821  funray  26904  funline  26906  bpolylem  26924  bpoly3  26934  bpoly4  26935  0hf  26948  waj-ax  26994  lukshef-ax2  26995  arg-ax  26996  limsucncmpi  27025  mblfinlem1  27099  mblfinlem2  27100  ismblfin  27103  voliunnfl  27106  cnambfre  27111  dvtanlem  27112  comppfsc  27250  neibastop2lem  27252  filnetlem3  27272  cover2  27278  abrexdom  27295  fdc  27312  cncfres  27337  heibor1lem  27381  bicontr  27553  tsim1  27575  moxfr  27664  mapfzcons1  27704  diophrw  27748  0dioph  27768  vdioph  27769  rabren3dioph  27805  2nn0ind  27937  rpnnen3  28032  kelac2lem  28068  frlmpwfi  28168  islinds2  28189  psgnunilem3  28325  psgnunilem4  28326  matsca  28376  lhe4.4ex1a  28452  rusbcALT  28542  ipo0  28554  ifr0  28555  fnchoice  28601  stoweidlem13  28662  stoweidlem34  28683  stirlinglem5  28727  stirlinglem13  28735  stirlingr  28739  aistia  28765  aisfina  28766  aiffnbandciffatnotciffb  28772  axorbciffatcxorb  28773  abnotbtaxb  28784  abnotataxb  28785  usgra2pthspth  29154  usgra2pthlem1  29159  wwlknext  29215  wwlknfi  29229  disjxwwlkn  29423  frgra0  29445  numclwwlkdisj  29532  numclwwlk3lem  29560  m2detleib  29624  ex-gte  29637  AnelBC  29672  empty-surprise  29709  eximp-surprise2  29712  vk15.4j  29802  2sb5nd  29838  dfvd1ir  29855  dfvd2anir  29867  dfvd2ir  29869  dfvd3ir  29876  dfvd3anir  29879  iden2  29906  e0bir  30080  uun2221p1  30117  uun2221p2  30118  2sb5ndVD  30215  2sb5ndALT  30237  iunconlem2  30240  bnj226  30294  bnj1101  30348  bnj110  30422  bnj149  30439  bnj150  30440  bnj151  30441  bnj517  30449  bnj580  30477  bnj865  30487  bnj900  30493  bnj996  30519  bnj1110  30544  bnj1133  30551  bnj1128  30552  bnj1145  30555  bnj1137  30557  bnj1171  30562  bnj1176  30567  bj-andnotimir  30637  bj-snsetex  30670  a6eNEW11  30745  sbtNEW11  30905  cbval2OLD11  31004  cbvex2OLD11  31005  nfsb4tw2AUXOLD11  31020  hlhilslem  34012
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 179
  Copyright terms: Public domain W3C validator