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

Theorem mpbir 209
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992.)
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 206 . 2
41, 3ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  pm5.74ri  246  con4bii  297  orri  376  imorri  414  imnani  423  mpbir2an  920  mpbir3an  1178  xorexmid  1379  tru  1399  nic-mpALT  1505  nic-ax  1506  nic-axALT  1507  mpgbir  1622  nfxfr  1645  19.35ri  1690  ax5e  1706  ax6ev  1749  exan  1973  cbvex2OLD  2029  ax13  2047  euequ1  2288  moanmo  2353  axi12  2433  axext2  2436  eqeltri  2541  nfcxfr  2617  neir  2657  neirr  2661  exmidneOLD  2663  nesymirOLD  2733  eqnetri  2753  nelir  2793  mprgbir  2821  vex  3112  issetri  3116  moeq  3275  cdeqi  3312  eqsstri  3533  3sstr4i  3542  rabrsn  4100  tpid1  4143  tpid2  4144  tpid3  4146  pwv  4248  uni0  4276  eqbrtri  4471  tr0  4556  trv  4557  zfrep4  4571  zfnuleu  4578  axnulALT  4579  0ex  4582  inex1  4593  0elpw  4621  axpow2  4632  axpow3  4633  pwex  4635  dvdemo1  4687  zfpair2  4692  exss  4715  moop2  4747  pwundif  4792  po0  4820  epse  4867  0elon  4936  relsnop  5112  relxp  5115  rel0  5132  relopabi  5133  eliunxp  5145  opeliunxp2  5146  dmi  5222  xpidtr  5394  xpima  5454  cnvcnv  5464  dmsn0  5480  cnvsn0  5481  funmpt  5629  funmpt2  5630  isarep2  5673  fresaunres2  5762  f0  5771  f10  5852  f1o00  5853  f1oi  5856  f1osn  5858  brprcneu  5864  opabiotafun  5934  fvopab3ig  5953  opabex  6141  eufnfv  6146  canth  6254  ncanth  6255  mpt2fun  6404  reldmmpt2  6413  ovid  6419  ovidig  6420  ovidi  6421  ovig  6424  ov3  6439  caovmo  6512  relmptopab  6523  porpss  6584  uniex2  6595  snnex  6606  tfinds2  6698  finds  6726  finds2  6728  oprabex  6788  oprabex3  6789  f1stres  6822  f2ndres  6823  relmpt2opab  6882  tpos0  7004  issmo  7038  tfrlem6  7070  tfrlem8  7072  tfrlem16  7081  tfr1a  7082  tfr1  7085  tz7.44lem1  7090  seqomlem2  7135  seqomlem3  7136  seqomlem4  7137  fnseqom  7139  0lt1o  7173  0we1  7175  eqer  7363  ecopover  7434  mapsnf1o3  7487  ssdomg  7581  ensn1  7599  snfi  7616  xpcomf1o  7626  map2xp  7707  limensuci  7713  sdom1  7739  unblem4  7795  fidomdm  7822  marypha1lem  7913  hartogslem1  7988  hartogs  7990  card2on  8001  ruALT  8049  inf2  8061  inf3lem6  8071  infeq5i  8074  zfinf2  8080  cantnflt  8112  cantnfltOLD  8142  cantnfOLD  8155  mapfienOLD  8159  cnfcom  8165  cnfcomOLD  8173  trcl  8180  tz9.1c  8182  tc2  8194  r1funlim  8205  r1fnon  8206  karden  8334  tskwe  8352  cardprclem  8381  pm54.43  8402  r0weon  8411  iunmapdisj  8425  alephfnon  8467  alephfplem4  8509  alephfp  8510  alephval3  8512  aceq3lem  8522  kmlem2  8552  cda1dif  8577  ackbij1  8639  ackbij2lem2  8641  ackbij2  8644  infpssrlem3  8706  hsmexlem4  8830  hsmexlem5  8831  axdc3lem4  8854  ac2  8862  axac3  8865  ac6  8881  axdclem2  8921  ondomon  8959  alephsucpw  8966  pwcfsdom  8979  cfpwsdom  8980  smobeth  8982  axpowndlem3  8996  axpowndlem3OLD  8997  zfcndun  9014  zfcndpow  9015  zfcndinf  9017  zfcndac  9018  wunex2  9137  uniwun  9139  wuncval2  9146  grur1  9219  axgroth5  9223  axgroth2  9224  axgroth6  9227  axgroth3  9230  grothtsk  9234  inaprc  9235  ltsopi  9287  dmaddpi  9289  dmmulpi  9290  1lt2pi  9304  nqerf  9329  addnqf  9347  mulnqf  9348  1lt2nq  9372  m1p1sr  9490  m1m1sr  9491  0lt1sr  9493  axaddf  9543  axmulf  9544  ax1cn  9547  subaddrii  9932  ixi  10203  recgt0ii  10476  nn1suc  10582  neg1lt0  10667  4d2e2  10717  arch  10817  un0mulcl  10855  nummac  11036  uzf  11113  indstr  11179  mnfltpnf  11364  ixxf  11568  ioof  11651  fzf  11705  fzp1disj  11767  fzp1nel  11791  fzof  11826  om2uzrani  12063  om2uzf1oi  12064  uzrdglem  12068  uzrdgfni  12069  uzrdg0i  12070  ltwenn  12073  hashgf1o  12081  axdc4uzlem  12092  sq0  12259  irec  12267  hashkf  12407  hashf  12412  hash0  12437  prhash2ex  12464  hashsslei  12484  hashxplem  12491  hashbclem  12501  hashf1lem1  12504  wrdexg  12557  wrd0  12565  revs1  12739  0csh0  12764  cshw1  12790  cats1fvn  12823  climmo  13380  fsumcom2  13589  ackbijnn  13640  incexclem  13648  infcvgaux1i  13668  fprodcom2  13788  efcvgfsum  13821  cos1bnd  13922  cos2bnd  13923  znnen  13946  qnnen  13947  aleph1re  13978  3dvds  14050  divalglem5  14055  bitsf  14077  sadcaddlem  14107  sadadd2lem  14109  sadadd3  14111  sadaddlem  14116  2prm  14233  phicl2  14298  pockthi  14425  unbenlem  14426  prmrec  14440  vdwlem13  14511  vdwnn  14516  ramcl2  14534  mod2xnegi  14557  modsubi  14558  structcnvcnv  14643  structfun  14644  setsres  14660  strfv  14666  strlemor1  14724  strleun  14727  0rest  14827  firest  14830  restid  14831  prdsval  14852  prdsbas  14854  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  prdsds  14861  imasaddfnlem  14925  imasvscafn  14934  oppchomfval  15109  oppcbas  15113  2oppchomf  15119  rescbas  15198  rescco  15201  rescabs  15202  0ssc  15206  0subcat  15207  idfucl  15250  wunnat  15325  homarel  15363  dmaf  15376  cdaf  15377  catcfuccl  15436  relxpchom  15450  catcxpccl  15476  oppchofcl  15529  oyoncl  15539  odubas  15763  letsr  15857  mgmidmo  15886  releqg  16248  ga0  16336  oppglem  16385  psgnunilem3  16521  psgnunilem4  16522  pmtrsn  16544  efgval  16735  efger  16736  efgsp1  16755  efgsfo  16757  efgredleme  16761  efgredlem  16765  efgred  16766  cygctb  16894  gsum2d2lem  17001  gsum2d2  17002  gsumcom2  17003  dprd2d2  17093  pgpfaclem1  17132  mgplem  17146  mgpress  17152  opprlem  17277  reldvdsr  17293  00lsp  17627  sralem  17823  srasca  17827  sravsca  17828  psrvscafval  18043  opsrbaslem  18142  psrbag0  18159  00ply1bas  18281  ply1plusgfvi  18283  xrsmgm  18453  zlmsca  18558  znbaslem  18577  resubdrg  18644  ocvfval  18697  ocv0  18708  cssval  18713  thlbas  18727  thlle  18728  islinds2  18848  matsca  18917  m2detleib  19133  eltopspOLD  19419  tgdom  19480  tgidm  19482  indistps2ALT  19515  restbas  19659  resttopon  19662  rest0  19670  leordtval2  19713  iocpnfordt  19716  icomnfordt  19717  iooordt  19718  cnpfval  19735  iscnp2  19740  ist1-3  19850  1stcfb  19946  islly2  19985  comppfsc  20033  1stckgen  20055  ptbasfi  20082  xkotf  20086  dfac14  20119  opnfbas  20343  hauspwpwf1  20488  alexsubALTlem4  20550  alexsubALT  20551  ptcmplem5  20556  cnextrel  20563  ust0  20722  tuslem  20770  0met  20869  prdsdsf  20870  prdsxmetlem  20871  prdsmet  20873  setsmsbas  20978  setsmsds  20979  prdsbl  20994  tngds  21162  qtopbaslem  21265  xrtgioo  21311  xrsdsre  21315  zcld  21318  recld2  21319  sszcld  21322  reperflem  21323  retopcon  21334  iccpnfcnv  21444  bndth  21458  ishtpy  21472  nmoleub2lem2  21599  recmet  21762  resscdrg  21798  ishl2  21810  recms  21812  volf  21940  iundisj2  21959  volsup  21966  icombl  21974  ioombl  21975  ismbf3d  22061  0plef  22079  0pledm  22080  itg1ge0  22093  mbfi1fseqlem5  22126  itg2addlem  22165  iblcnlem1  22194  reldv  22274  limciun  22298  dvexp  22356  dveflem  22380  lhop1lem  22414  lhop  22417  elply2  22593  elplyd  22599  ply1term  22601  ply0  22605  plymullem  22613  qaa  22719  pserulm  22817  pserdvlem2  22823  efcn  22838  sincosq1lem  22890  tangtx  22898  sincos4thpi  22906  sincos6thpi  22908  pige3  22910  efif1olem4  22932  logf1o  22952  relogf1o  22954  log1  22970  loge  22971  relogiso  22982  dvrelog  23018  relogcn  23019  logcn  23028  cxpcn3  23122  resqrtcn  23123  leibpi  23273  log2ublem1  23277  birthday  23284  emcllem5  23329  harmonicbnd  23333  harmonicbnd2  23334  emgt0  23336  harmonicbnd3  23337  ppiltx  23451  ppiublem1  23477  ppiub  23479  bclbnd  23555  bpos1lem  23557  bposlem8  23566  lgsquadlem2  23630  2sqlem9  23648  2sqlem10  23649  chebbnd1  23657  selberg2lem  23735  pntrsumo1  23750  selbergsb  23760  pntpbnd  23773  istrkg2ld  23858  ttgval  24178  ttglem  24179  cchhllem  24190  ax5seglem7  24238  axlowdimlem4  24248  axlowdimlem6  24250  axlowdimlem7  24251  axlowdimlem10  24254  axlowdimlem13  24257  axlowdimlem16  24260  uhgra0  24309  umgra0  24325  usgra0  24370  usgra1v  24390  cusgraexilem2  24467  cusgrasizeindslem2  24474  0wlk  24547  0trl  24548  wlkntrllem2  24562  wlkntrl  24564  0pth  24572  1pthonlem1  24591  usgrcyclnl2  24641  4cycl4dv  24667  wwlknext  24724  wwlknfi  24738  disjxwwlkn  24745  vdgrf  24898  umgrabi  24983  vdegp1ai  24984  vdegp1bi  24985  konigsberg  24987  frgra0  24994  numclwwlkdisj  25080  numclwwlk3lem  25108  ex-dif  25144  ex-in  25146  ex-eprel  25154  ex-id  25155  ex-fl  25168  avril1  25171  2bornot2b  25172  grposn  25217  issubgoi  25312  0vfval  25499  vsfval  25528  ajmoi  25774  ajfuni  25775  normlem2  26028  norm3adifii  26065  hhip  26094  hlim0  26153  hlimcaui  26154  hlimf  26155  hhssnv  26180  shscli  26235  shsval2i  26305  h1de2i  26471  fh3i  26541  fh4i  26542  cm2mi  26544  qlaxr3i  26554  mayetes3i  26648  ho0f  26670  hoif  26673  hodidi  26706  ho0subi  26714  hosd1i  26741  adjmo  26751  nmopsetn0  26784  nmfnsetn0  26797  funadj  26805  funcnvadj  26812  nmcexi  26945  cnlnadjlem8  26993  nmoptri2i  27018  opsqrlem4  27062  hmopidmchi  27070  pjoci  27099  pjinvari  27110  abrexdomjm  27405  elim2ifim  27423  iundisj2f  27449  rinvf1o  27472  funcnvmptOLD  27509  dfcnv2  27517  snct  27534  dmct  27537  fpwrelmap  27556  iundisj2fi  27602  gsumle  27770  xrge0pluscn  27922  zlmds  27945  zlmtset  27946  qqhre  27998  esumfsup  28076  esumpcvgval  28084  hasheuni  28091  esumcvg  28092  dmsigagen  28144  measvuni  28185  voliune  28201  volfiniune  28202  br2base  28240  dya2iocuni  28254  oms0  28266  eulerpartlem1  28306  eulerpartlemt  28310  eulerpartgbij  28311  fib0  28338  coinfliprv  28421  ballotlem2  28427  ballotlemic  28445  ballotlem7  28474  ballotth  28476  plymul02  28503  lgamgulm2  28578  lgamcvglem  28582  gamf  28585  subfacp1lem5  28628  subfacp1lem6  28629  kur14lem9  28658  cvmcov2  28720  cvmliftlem1  28730  cvmliftlem4  28733  cvmliftlem5  28734  msrfo  28906  problem5  29023  ghomgrpilem2  29026  relexp0  29052  relexpsucr  29053  relexpsucl  29055  dfrtrclrec2  29066  rtrclreclem.refl  29067  rtrclreclem.subset  29068  rtrclreclem.min  29070  dfrtrcl2  29071  brtpid1  29098  brtpid2  29099  brtpid3  29100  logi  29121  faclimlem1  29168  domep  29225  axextndbi  29237  poseq  29333  wfrlem6  29348  wfrlem14  29356  wfrlem16  29358  frrlem10  29398  sltval2  29416  brv  29527  txprel  29529  relsset  29538  relbigcup  29547  fvbigcup  29552  fnsingle  29569  fvsingle  29570  snelsingles  29572  funimage  29578  fullfunfnv  29596  imagesset  29603  funtransport  29681  colinrel  29707  funray  29790  funline  29792  bpolylem  29810  bpoly3  29820  bpoly4  29821  0hf  29834  waj-ax  29879  lukshef-ax2  29880  arg-ax  29881  limsucncmpi  29910  mblfinlem1  30051  mblfinlem2  30052  ismblfin  30055  voliunnfl  30058  cnambfre  30063  dvtanlem  30064  neibastop2lem  30178  filnetlem3  30198  cover2  30204  abrexdom  30221  fdc  30238  cncfres  30261  heibor1lem  30305  bicontr  30477  an12i  30498  tsim1  30537  ac6s6f  30581  moxfr  30624  mapfzcons1  30649  diophrw  30692  0dioph  30712  vdioph  30713  rabren3dioph  30749  2nn0ind  30881  rpnnen3  30974  kelac2lem  31010  frlmpwfi  31046  3lcm2e6  31219  lhe4.4ex1a  31234  rusbcALT  31346  ipo0  31358  ifr0  31359  fnchoice  31404  fprodn0f  31594  fprodge0  31597  fprodge1  31598  resincncf  31677  dvnprodlem3  31745  mbf0  31756  volioc  31771  stoweidlem13  31795  stoweidlem34  31816  stirlinglem5  31860  stirlinglem13  31868  stirlingr  31872  fourierdlem42  31931  fourierdlem62  31951  fouriersw  32014  etransc  32066  aistia  32092  aisfina  32093  aiffnbandciffatnotciffb  32099  axorbciffatcxorb  32100  abnotbtaxb  32111  abnotataxb  32112  usgra2pthspth  32351  usgra2pthlem1  32353  uhg0e  32376  oddinmgm  32503  2zrngamgm  32745  2zrngaabl  32750  2zrngmmgm  32752  2zrngnring  32758  fldhmsubc  32892  fldhmsubcOLD  32911  eliunxp2  32923  zlmodzxzldeplem  33099  zlmodzxzldep  33105  ldepslinc  33110  ex-gte  33123  empty-surprise  33197  eximp-surprise2  33200  vk15.4j  33298  2sb5nd  33333  dfvd1ir  33350  dfvd2anir  33361  dfvd2ir  33363  dfvd3ir  33370  dfvd3anir  33373  iden2  33400  e0bir  33574  uun2221p1  33611  uun2221p2  33612  2sb5ndVD  33710  2sb5ndALT  33732  iunconlem2  33735  bnj226  33789  bnj1101  33843  bnj110  33916  bnj149  33933  bnj150  33934  bnj151  33935  bnj517  33943  bnj580  33971  bnj865  33981  bnj900  33987  bnj996  34013  bnj1110  34038  bnj1133  34045  bnj1128  34046  bnj1145  34049  bnj1137  34051  bnj1171  34056  bnj1176  34061  bj-babylob  34192  bj-nalnalimiOLD  34223  bj-nfv  34227  bj-dvdemo1  34388  bj-disjcsn  34505  bj-snsetex  34521  bj-0eltag  34536  bj-2upln0  34581  bj-2upln1upl  34582  elimhyps  34692  dedths  34693  renegclALT  34694  hlhilslem  37668  xphe  37804  0he  37805  he0  37807  snhesn  37809  idhe  37810  frege54cor1c  37942
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 185
  Copyright terms: Public domain W3C validator