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  1137  tru  1331  nic-mpALT  1447  nic-ax  1448  nic-axALT  1449  mpto2OLD  1545  mtp-xor  1546  mtp-xorOLD  1547  mpgbir  1560  nfxfr  1580  19.35ri  1614  a9ev  1671  exiftruOLD  1673  exan  1908  cbval2OLD  1995  cbvex2  1996  ax12  2027  a9eOLD  2042  sbtOLD  2137  sbie  2160  moaneu  2351  moanmo  2352  axi12  2426  axext2  2429  eqeltri  2517  nfcxfr  2580  neir  2615  neirr  2617  exmidne  2618  eqnetri  2629  nesymir  2653  nelir  2709  mprgbir  2787  vex  2972  issetri  2976  moeq  3123  cdeqi  3159  eqsstri  3371  3sstr4i  3380  tpid1  3949  tpid2  3950  tpid3  3952  pwv  4046  uni0  4073  eqbrtri  4266  tr0  4351  trv  4352  zfrep4  4366  zfnuleu  4373  axnulALT  4374  0ex  4377  inex1  4387  0elpw  4412  axpow2  4422  axpow3  4423  pwex  4425  dvdemo1  4442  zfpair2  4447  exss  4469  moop2  4494  pwundif  4535  po0  4563  epse  4610  0elon  4679  uniex2  4749  snnex  4758  tfinds2  4888  finds  4916  finds2  4918  relsnop  5026  relxp  5029  rel0  5045  relopabi  5046  eliunxp  5058  opeliunxp2  5059  dmi  5132  xpidtr  5304  xpima  5361  cnvcnv  5371  dmsn0  5387  cnvsn0  5388  funmpt  5540  funmpt2  5541  isarep2  5584  fresaunres2  5666  f0  5678  f10  5760  f1o00  5761  f1oi  5764  f1osn  5766  brprcneu  5772  fvopab3ig  5855  opabex  6016  eufnfv  6024  mpt2fun  6226  reldmmpt2  6235  oprabex  6241  oprabex3  6242  ovid  6244  ovidig  6245  ovidi  6246  ovig  6249  ov3  6264  caovmo  6338  relmptopab  6346  f1stres  6422  f2ndres  6423  relmpt2opab  6483  tpos0  6563  porpss  6580  opabiotafun  6590  canth  6593  ncanth  6594  issmo  6663  tfrlem6  6696  tfrlem8  6698  tfrlem16  6707  tfr1a  6708  tfr1  6711  tz7.44lem1  6716  seqomlem2  6761  seqomlem3  6762  seqomlem4  6763  fnseqom  6765  abianfp  6769  0lt1o  6801  0we1  6803  eqer  6991  ecopover  7061  th3qcor  7065  mapsnf1o3  7115  ssdomg  7206  ensn1  7224  snfi  7240  xpcomf1o  7250  map2xp  7330  limensuci  7336  sdom1  7361  unblem4  7415  fidomdm  7441  marypha1lem  7491  hartogslem1  7564  hartogs  7566  card2on  7575  ruALT  7622  inf2  7631  inf3lem6  7641  infeq5i  7644  zfinf2  7650  cantnflt  7680  cantnf  7702  mapfien  7706  cnfcom  7710  trcl  7717  tz9.1c  7719  tc2  7734  r1funlim  7745  r1fnon  7746  karden  7874  tskwe  7892  cardprclem  7921  pm54.43  7942  r0weon  7949  iunmapdisj  7959  alephfnon  8001  alephfplem4  8043  alephfp  8044  alephval3  8046  aceq3lem  8056  kmlem2  8086  cda1dif  8111  ackbij1  8173  ackbij2lem2  8175  ackbij2  8178  infpssrlem3  8240  hsmexlem4  8364  hsmexlem5  8365  axdc3lem4  8388  ac2  8396  axac3  8399  ac6  8415  axdclem2  8455  ondomon  8493  alephsucpw  8500  pwcfsdom  8513  cfpwsdom  8514  smobeth  8516  axpowndlem3  8529  zfcndun  8545  zfcndpow  8546  zfcndinf  8548  zfcndac  8549  wunex2  8668  uniwun  8670  wuncval2  8677  grur1  8750  axgroth5  8754  axgroth2  8755  axgroth6  8758  axgroth3  8761  grothtsk  8765  inaprc  8766  ltsopi  8820  dmaddpi  8822  dmmulpi  8823  1lt2pi  8837  nqerf  8862  addnqf  8880  mulnqf  8881  1lt2nq  8905  m1p1sr  9022  m1m1sr  9023  0lt1sr  9025  axaddf  9075  axmulf  9076  ax1cn  9079  subaddrii  9444  ixi  9706  recgt0ii  9971  nn1suc  10076  4d2e2  10187  arch  10273  un0mulcl  10309  nummac  10469  uzf  10546  indstr  10600  mnfltpnf  10778  ixxf  10981  ioof  11057  fzf  11102  fzp1disj  11160  fzof  11192  om2uzrani  11347  om2uzf1oi  11348  uzrdglem  11352  uzrdgfni  11353  uzrdg0i  11354  ltwenn  11357  hashgf1o  11365  axdc4uzlem  11376  sq0  11528  irec  11535  hashkf  11675  hashf  11680  hash0  11701  hashsslei  11740  hashxplem  11751  hashbclem  11756  hashf1lem1  11759  wrd0  11787  wrdexg  11794  revs1  11852  cats1fvn  11877  climmo  12406  fsumcom2  12613  ackbijnn  12662  incexclem  12671  infcvgaux1i  12691  efcvgfsum  12743  cos1bnd  12843  cos2bnd  12844  znnen  12867  qnnen  12868  aleph1re  12899  nthruz  12906  dvdslelem  12949  3dvds  12967  divalglem5  12972  bitsf  12994  sadcaddlem  13024  sadadd2lem  13026  sadadd3  13028  sadaddlem  13033  isprm3  13143  2prm  13150  phicl2  13212  pockthi  13330  unbenlem  13331  prmrec  13345  vdwlem13  13416  vdwnn  13421  ramcl2  13439  mod2xnegi  13462  modsubi  13463  structcnvcnv  13535  structfun  13536  setsres  13550  strfv  13556  strlemor1  13611  strleun  13614  0rest  13712  firest  13715  restid  13716  prdsval  13733  prdsbas  13735  prdsplusg  13736  prdsmulr  13737  prdsvsca  13738  prdsds  13741  imasaddfnlem  13808  imasvscafn  13817  oppchomfval  13995  oppcbas  13999  2oppchomf  14005  rescbas  14084  rescco  14087  rescabs  14088  idfucl  14133  wunnat  14208  homarel  14246  dmaf  14259  cdaf  14260  catcfuccl  14319  relxpchom  14333  catcxpccl  14359  oppchofcl  14412  oyoncl  14422  odubas  14615  letsr  14708  mgmidmo  14729  releqg  15023  ga0  15111  oppglem  15182  efgval  15385  efger  15386  efgsp1  15405  efgsfo  15407  efgredleme  15411  efgredlem  15415  efgred  15416  cygctb  15537  gsum2d2lem  15583  gsum2d2  15584  gsumcom2  15585  dprd2d2  15638  pgpfaclem1  15675  mgplem  15689  mgpress  15695  opprlem  15769  reldvdsr  15785  00lsp  16093  sralem  16285  srasca  16289  psrvscafval  16490  opsrbaslem  16574  psrbag0  16590  00ply1bas  16670  ply1plusgfvi  16672  zlmsca  16838  znbaslem  16855  ocvfval  16929  ocv0  16940  cssval  16945  thlbas  16959  thlle  16960  eltopspOLD  17019  tgdom  17079  tgidm  17081  indistps2ALT  17114  restbas  17258  resttopon  17261  rest0  17269  leordtval2  17312  iocpnfordt  17315  icomnfordt  17316  iooordt  17317  cnpfval  17334  iscnp2  17339  ist1-3  17449  1stcfb  17544  islly2  17583  1stckgen  17622  ptbasfi  17649  xkotf  17653  dfac14  17686  opnfbas  17910  hauspwpwf1  18055  alexsubALTlem4  18117  alexsubALT  18118  ptcmplem5  18123  cnextrel  18130  ust0  18285  tuslem  18333  0met  18432  prdsdsf  18433  prdsxmetlem  18434  prdsmet  18436  setsmsbas  18541  setsmsds  18542  prdsbl  18557  tngds  18725  qtopbaslem  18828  xrtgioo  18873  xrsdsre  18877  zcld  18880  recld2  18881  sszcld  18884  reperflem  18885  retopcon  18896  iccpnfcnv  19005  bndth  19019  ishtpy  19033  nmoleub2lem2  19160  recmet  19312  resscdrg  19348  ishl2  19360  volf  19461  iundisj2  19479  volsup  19486  icombl  19494  ioombl  19495  ismbf3d  19580  0plef  19598  0pledm  19599  itg1ge0  19612  mbfi1fseqlem5  19645  itg2addlem  19684  iblcnlem1  19713  reldv  19793  limciun  19817  dvexp  19875  dveflem  19899  lhop1lem  19933  lhop  19936  elply2  20151  elplyd  20157  ply1term  20159  ply0  20163  plymullem  20171  qaa  20276  pserulm  20374  pserdvlem2  20380  efcn  20395  sincosq1lem  20441  tangtx  20449  sincos4thpi  20457  sincos6thpi  20459  pige3  20461  efif1olem4  20483  logf1o  20498  relogf1o  20500  log1  20516  loge  20517  relogiso  20528  dvrelog  20564  relogcn  20565  logcn  20574  cxpcn3  20668  resqrcn  20669  leibpi  20818  log2ublem1  20822  birthday  20829  emcllem5  20874  harmonicbnd  20878  harmonicbnd2  20879  emgt0  20881  harmonicbnd3  20882  ppiltx  20996  ppiublem1  21022  ppiub  21024  bclbnd  21100  bpos1lem  21102  bposlem8  21111  lgsquadlem2  21175  2sqlem9  21193  2sqlem10  21194  chebbnd1  21202  selberg2lem  21280  pntrsumo1  21295  selbergsb  21305  pntpbnd  21318  uhgra0  21380  umgra0  21396  usgra0  21426  usgra1v  21445  cusgraexilem2  21512  cusgrasizeindslem2  21519  0wlk  21581  0trl  21582  wlkntrllem2  21596  wlkntrl  21598  0pth  21606  1pthonlem1  21625  usgrcyclnl2  21664  4cycl4dv  21690  vdgrf  21705  umgrabi  21741  vdegp1ai  21742  vdegp1bi  21743  konigsberg  21745  ex-dif  21767  ex-in  21769  ex-eprel  21777  ex-id  21778  ex-fl  21791  avril1  21793  2bornot2b  21794  grposn  21839  issubgoi  21934  0vfval  22121  vsfval  22150  ajmoi  22396  ajfuni  22397  normlem2  22649  norm3adifii  22686  hhip  22715  hlim0  22774  hlimcaui  22775  hlimf  22776  hhssnv  22800  shscli  22855  shsval2i  22925  h1de2i  23091  fh3i  23161  fh4i  23162  cm2mi  23164  qlaxr3i  23174  mayetes3i  23268  ho0f  23290  hoif  23293  hodidi  23326  ho0subi  23334  hosd1i  23361  adjmo  23371  nmopsetn0  23404  nmfnsetn0  23417  funadj  23425  funcnvadj  23432  nmcexi  23565  cnlnadjlem8  23613  nmoptri2i  23638  opsqrlem4  23682  hmopidmchi  23690  pjoci  23719  pjinvari  23730  abrexdomjm  24031  elim2ifim  24050  iundisj2f  24075  rinvf1o  24093  funcnvmptOLD  24134  dfcnv2  24142  snct  24161  dmct  24164  fpwrelmap  24184  iundisj2fi  24226  nn0srg  24375  rge0srg  24376  gsumle  24410  reofld  24490  rearchi  24492  xrge0slmod  24493  xrge0iifcnv  24532  xrge0pluscn  24539  recms  24557  zlmds  24562  zlmtset  24563  cnzh  24568  rezh  24569  qqhre  24615  esumfsup  24690  esumpcvgval  24698  hasheuni  24705  esumcvg  24706  dmsigagen  24757  measvuni  24798  voliune  24815  volfiniune  24816  br2base  24849  dya2iocuni  24863  eulerpartlem1  24909  eulerpartlemt  24913  eulerpartgbij  24914  eulerpartlemgh  24920  coinfliprv  25000  ballotlem2  25006  ballotlemfc0  25010  ballotlemfcc  25011  ballotlemic  25024  ballotlem7  25053  ballotth  25055  lgamgulm2  25080  lgamcvglem  25084  gamf  25087  subfacp1lem5  25130  subfacp1lem6  25131  kur14lem9  25160  cvmcov2  25222  cvmliftlem1  25232  cvmliftlem4  25235  cvmliftlem5  25236  ghomgrpilem2  25357  relexp0  25389  relexpsucr  25390  relexpsucl  25392  dfrtrclrec2  25403  rtrclreclem.refl  25404  rtrclreclem.subset  25405  rtrclreclem.min  25407  dfrtrcl2  25408  brtpid1  25438  brtpid2  25439  brtpid3  25440  fzp1nel  25470  fprodcom2  25568  faclimlem1  25622  domep  25680  axextndbi  25692  poseq  25788  wfrlem6  25803  wfrlem14  25811  wfrlem16  25813  frrlem10  25853  sltval2  25871  nosgnn0i  25874  brv  25982  txprel  25984  relsset  25993  relbigcup  26002  fvbigcup  26007  fnsingle  26024  fvsingle  26025  snelsingles  26027  funimage  26033  fullfunfnv  26051  imagesset  26058  ax5seglem7  26134  axlowdimlem4  26144  axlowdimlem6  26146  axlowdimlem7  26147  axlowdimlem10  26150  axlowdimlem13  26153  axlowdimlem16  26156  axlowdimlem17  26157  axlowdim  26160  funtransport  26225  colinrel  26251  funray  26334  funline  26336  bpolylem  26354  bpoly3  26364  bpoly4  26365  0hf  26378  waj-ax  26424  lukshef-ax2  26425  arg-ax  26426  limsucncmpi  26455  mblfinlem1  26508  mblfinlem2  26509  ismblfin  26512  voliunnfl  26515  cnambfre  26520  dvtanlem  26521  comppfsc  26654  neibastop2lem  26656  filnetlem3  26676  cover2  26682  abrexdom  26699  fdc  26716  cncfres  26741  heibor1lem  26785  bicontr  26957  tsim1  26979  moxfr  27070  mapfzcons1  27110  diophrw  27154  0dioph  27174  vdioph  27175  rabren3dioph  27211  2nn0ind  27343  rpnnen3  27438  kelac2lem  27474  frlmpwfi  27574  islinds2  27595  psgnunilem3  27731  psgnunilem4  27732  matsca  27782  lhe4.4ex1a  27858  rusbcALT  27951  ipo0  27963  ifr0  27964  fnchoice  28010  stoweidlem13  28072  stoweidlem34  28093  stirlinglem5  28137  stirlinglem13  28145  stirlingr  28149  aistia  28175  aisfina  28176  aiffnbandciffatnotciffb  28182  axorbciffatcxorb  28183  abnotbtaxb  28194  abnotataxb  28195  cshw1  28629  usgra2pthspth  28663  usgra2pthlem1  28668  frgra0  28778  ex-gte  28866  AnelBC  28901  vk15.4j  29006  2sb5nd  29042  dfvd1ir  29059  dfvd2anir  29071  dfvd2ir  29073  dfvd3ir  29080  dfvd3anir  29083  iden2  29110  e0bir  29284  uun2221p1  29321  uun2221p2  29322  2sb5ndVD  29419  2sb5ndALT  29441  iunconlem2  29444  bnj226  29498  bnj1101  29552  bnj110  29626  bnj149  29643  bnj150  29644  bnj151  29645  bnj517  29653  bnj580  29681  bnj865  29691  bnj900  29697  bnj996  29723  bnj1110  29748  bnj1133  29755  bnj1128  29756  bnj1145  29759  bnj1137  29761  bnj1171  29766  bnj1176  29771  a9eNEW7  29867  sbtNEW7  30028  cbval2OLD7  30127  cbvex2OLD7  30128  nfsb4tw2AUXOLD7  30143  hlhilslem  33135
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