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

Theorem mpbir 221
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 218 . 2 (𝜓𝜑)
41, 3ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 196
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 197
This theorem is referenced by:  pm5.74ri  261  con4bii  310  orri  390  imorri  429  imnani  438  mpbir2an  993  mpbir3an  1427  xorexmid  1629  tru  1636  had1  1691  nic-mpALT  1746  nic-ax  1747  nic-axALT  1748  nfi  1863  mpgbir  1875  nfxfr  1928  19.35ri  1956  nfxfrOLD  1986  ax5e  1990  ax6ev  2056  exanOLDOLD  2314  ax13  2394  ax13ALT  2450  euequ1  2613  moanmo  2670  axi12  2738  axext2  2741  eqeltri  2835  nfcxfr  2900  neir  2935  neirr  2941  eqnetri  3002  nelir  3038  mprgbir  3065  vex  3343  issetri  3350  moeq  3523  rmoeq  3546  cdeqi  3561  eqsstri  3776  3sstr4i  3785  rabnc  4105  tpid1  4447  tpid2  4448  pwv  4585  uni0  4617  int0  4642  eqbrtri  4825  tr0  4916  trv  4917  zfrep4  4931  zfnuleu  4938  axnulALT  4939  0ex  4942  inex1  4951  elpwi2  4978  0elpw  4983  axpow2  4994  axpow3  4995  pwex  4997  dvdemo1  5051  zfpair2  5056  exss  5080  brv  5089  opwo0id  5109  moop2  5114  pwundif  5171  0sn0ep  5183  po0  5202  epse  5249  relxp  5283  relsnopOLD  5385  rel0  5399  relopabi  5401  relopabiALT  5402  eliunxp  5415  opeliunxp2  5416  dmi  5495  xpidtr  5676  xpima  5734  cnvcnv  5744  cnvcnvOLD  5745  dmsn0  5760  cnvsn0  5761  0elon  5939  funmpt  6087  funmpt2  6088  funcnv0  6116  isarep2  6139  fresaunres2  6237  f0  6247  f10  6330  f10d  6331  f1o00  6332  f1oi  6335  f1osn  6337  brprcneu  6345  opabiotafun  6421  fvopab3ig  6440  opabex  6647  mptexgf  6649  eufnfv  6654  isof1oopb  6738  canth  6771  ncanth  6772  mpt2fun  6927  reldmmpt2  6936  ovid  6942  ovidig  6943  ovidi  6944  ovig  6947  ov3  6962  caovmo  7036  relmptopab  7048  porpss  7106  uniex2  7117  snnexOLD  7132  tfinds2  7228  finds  7257  finds2  7259  oprabex  7321  oprabex3  7322  f1stres  7357  f2ndres  7358  relmpt2opab  7427  opeliunxp2f  7505  tpos0  7551  wfrrel  7589  wfrlem14  7597  wfrlem16  7599  issmo  7614  tfrlem6  7647  tfrlem8  7649  tfrlem16  7658  tfr1a  7659  tfr1  7662  tz7.44lem1  7670  seqomlem2  7715  seqomlem3  7716  seqomlem4  7717  fnseqom  7719  0lt1o  7753  0we1  7755  eqer  7946  ecopover  8018  mapsnf1o3  8072  ssdomg  8167  ensn1  8185  snfi  8203  xpcomf1o  8214  map2xp  8295  limensuci  8301  sdom1  8325  unblem4  8380  fidomdm  8408  marypha1lem  8504  hartogslem1  8612  hartogs  8614  card2on  8624  nelaneq  8669  epinid0  8670  ruALT  8673  cnvepnep  8676  inf2  8693  inf3lem6  8703  infeq5i  8706  zfinf2  8712  cantnflt  8742  cnfcom  8770  trcl  8777  tz9.1c  8779  tc2  8791  r1funlim  8802  r1fnon  8803  karden  8931  tskwe  8966  cardprclem  8995  pm54.43  9016  r0weon  9025  iunmapdisj  9036  alephfnon  9078  alephfplem4  9120  alephfp  9121  alephval3  9123  aceq3lem  9133  kmlem2  9165  cda1dif  9190  ackbij1  9252  ackbij2lem2  9254  ackbij2  9257  infpssrlem3  9319  hsmexlem4  9443  hsmexlem5  9444  axdc3lem4  9467  ac2  9475  axac3  9478  ac6  9494  axdclem2  9534  dmct  9538  ondomon  9577  alephsucpw  9584  pwcfsdom  9597  cfpwsdom  9598  smobeth  9600  axpowndlem3  9613  zfcndun  9629  zfcndpow  9630  zfcndinf  9632  zfcndac  9633  wunex2  9752  uniwun  9754  wuncval2  9761  grur1  9834  axgroth5  9838  axgroth2  9839  axgroth6  9842  axgroth3  9845  grothtsk  9849  inaprc  9850  ltsopi  9902  dmaddpi  9904  dmmulpi  9905  1lt2pi  9919  nqerf  9944  addnqf  9962  mulnqf  9963  1lt2nq  9987  m1p1sr  10105  m1m1sr  10106  0lt1sr  10108  axaddf  10158  axmulf  10159  ax1cn  10162  subaddrii  10562  ixi  10848  recgt0ii  11121  nn1suc  11233  neg1lt0  11319  4d2e2  11376  arch  11481  un0mulcl  11519  pnf0xnn0  11562  3halfnz  11648  nummac  11750  uzf  11882  indstr  11949  mnfltpnf  12153  ixxf  12378  ioof  12464  fzf  12523  0nelfz1  12553  fzp1disj  12592  fzp1nel  12617  fzof  12661  om2uzrani  12945  om2uzf1oi  12946  uzrdglem  12950  uzrdgfni  12951  uzrdg0i  12952  ltwenn  12955  hashgf1o  12964  axdc4uzlem  12976  sq0  13149  irec  13158  facmapnn  13266  hashkf  13313  hashfxnn0  13318  hashf  13319  hashfOLD  13320  hash0  13350  prhash2ex  13379  hashsslei  13405  hashxplem  13412  hashbclem  13428  hashf1lem1  13431  wrdexg  13501  s1dm  13579  revs1  13714  0csh0  13739  cshw1  13768  cats1fvn  13803  s2dm  13835  funcnvs1  13857  relexp0g  13961  relexpsucnnr  13964  dfrtrclrec2  13996  rtrclreclem1  13997  rtrclreclem2  13998  rtrclreclem4  14000  dfrtrcl2  14001  climmo  14487  fsumcom2  14704  fsumcom2OLD  14705  ackbijnn  14759  incexclem  14767  infcvgaux1i  14788  fprodcom2  14913  fprodcom2OLD  14914  fprodn0f  14921  fprodge0  14923  fprodge1  14925  bpolylem  14978  bpoly3  14988  bpoly4  14989  efcvgfsum  15015  cos1bnd  15116  cos2bnd  15117  znnen  15140  qnnen  15141  aleph1re  15173  3dvds  15254  3dvdsOLD  15255  n2dvdsm1  15307  n2dvds3  15309  divalglem5  15322  flodddiv4  15339  bitsf  15351  sadcaddlem  15381  sadadd2lem  15383  sadadd3  15385  sadaddlem  15390  lcmf0  15549  lcmfunsnlem2lem1  15553  lcmfunsnlem2  15555  coprmprod  15577  coprmproddvdslem  15578  2prm  15607  3lcm2e6  15642  phicl2  15675  pockthi  15813  unbenlem  15814  prmrec  15828  vdwlem13  15899  vdwnn  15904  ramcl2  15922  prmgapprmo  15968  mod2xnegi  15977  modsubi  15978  prmo4  16037  prmo5  16038  prmo6  16039  structcnvcnv  16073  setsres  16103  strfv  16109  strlemor1OLD  16171  strleun  16174  0rest  16292  firest  16295  restid  16296  prdsval  16317  prdsbas  16319  prdsplusg  16320  prdsmulr  16321  prdsvsca  16322  prdsds  16326  imasaddfnlem  16390  imasvscafn  16399  oppchomfval  16575  oppcbas  16579  2oppchomf  16585  rescbas  16690  rescco  16693  rescabs  16694  0ssc  16698  0subcat  16699  idfucl  16742  wunnat  16817  homarel  16887  dmaf  16900  cdaf  16901  catcfuccl  16960  relxpchom  17022  catcxpccl  17048  oppchofcl  17101  oyoncl  17111  odubas  17334  letsr  17428  mgmidmo  17460  releqg  17842  ga0  17931  oppglem  17980  psgnunilem3  18116  psgnunilem4  18117  pmtrsn  18139  efgval  18330  efger  18331  efgsp1  18350  efgsfo  18352  efgredleme  18356  efgredlem  18360  efgred  18361  cygctb  18493  gsum2d2lem  18572  gsum2d2  18573  gsumcom2  18574  dprd2d2  18643  pgpfaclem1  18680  mgplem  18694  mgpress  18700  opprlem  18828  reldvdsr  18844  00lsp  19183  sralem  19379  srasca  19383  sravsca  19384  psrvscafval  19592  opsrbaslem  19679  opsrbaslemOLD  19680  psrbag0  19696  00ply1bas  19812  ply1plusgfvi  19814  cnfldfun  19960  cnfldfunALT  19961  xrsmgm  19983  zlmsca  20071  znbaslem  20088  znbaslemOLD  20089  resubdrg  20156  ocvfval  20212  ocv0  20223  cssval  20228  thlbas  20242  thlle  20243  islinds2  20354  matsca  20423  m2detleib  20639  tgdom  20984  tgidm  20986  indistps2ALT  21020  restbas  21164  resttopon  21167  rest0  21175  leordtval2  21218  iocpnfordt  21221  icomnfordt  21222  iooordt  21223  cnpfval  21240  iscnp2  21245  ist1-3  21355  1stcfb  21450  islly2  21489  comppfsc  21537  1stckgen  21559  ptbasfi  21586  xkotf  21590  dfac14  21623  opnfbas  21847  hauspwpwf1  21992  alexsubALTlem4  22055  alexsubALT  22056  ptcmplem5  22061  cnextrel  22068  ust0  22224  tuslem  22272  0met  22372  prdsdsf  22373  prdsxmetlem  22374  prdsmet  22376  setsmsbas  22481  setsmsds  22482  prdsbl  22497  tngds  22653  qtopbaslem  22763  xrtgioo  22810  xrsdsre  22814  zcld  22817  recld2  22818  sszcld  22821  reperflem  22822  retopconn  22833  iccpnfcnv  22944  bndth  22958  ishtpy  22972  nmoleub2lem2  23116  zclmncvs  23148  recmet  23320  resscdrg  23354  ishl2  23366  recms  23368  volf  23497  iundisj2  23517  volsup  23524  icombl  23532  ioombl  23533  ismbf3d  23620  0plef  23638  0pledm  23639  itg1ge0  23652  mbfi1fseqlem5  23685  itg2addlem  23724  iblcnlem1  23753  reldv  23833  limciun  23857  dvexp  23915  dveflem  23941  lhop1lem  23975  lhop  23978  elply2  24151  elplyd  24157  ply1term  24159  ply0  24163  plymullem  24171  qaa  24277  pserulm  24375  pserdvlem2  24381  efcn  24396  sincosq1lem  24448  tangtx  24456  sincos4thpi  24464  sincos6thpi  24466  pige3  24468  efif1olem4  24490  logf1o  24510  relogf1o  24512  log1  24531  loge  24532  relogiso  24543  dvrelog  24582  relogcn  24583  logcn  24592  cxpcn3  24688  resqrtcn  24689  leibpi  24868  log2ublem1  24872  birthday  24880  emcllem5  24925  harmonicbnd  24929  harmonicbnd2  24930  emgt0  24932  harmonicbnd3  24933  lgamgulm2  24961  lgamcvglem  24965  gamf  24968  ppiltx  25102  ppiublem1  25126  ppiub  25128  bclbnd  25204  bpos1lem  25206  bposlem8  25215  lgsquadlem2  25305  2sqlem9  25351  2sqlem10  25352  chebbnd1  25360  selberg2lem  25438  pntrsumo1  25453  selbergsb  25463  pntpbnd  25476  istrkg2ld  25558  tgcgr4  25625  ttgval  25954  ttglem  25955  cchhllem  25966  ax5seglem7  26014  axlowdimlem4  26024  axlowdimlem6  26026  axlowdimlem7  26027  axlowdimlem10  26030  axlowdimlem13  26033  axlowdimlem16  26036  uhgr0e  26165  uhgr0  26167  upgrbi  26187  umgrbi  26195  usgr0  26334  lfuhgr1v0e  26345  usgrexmpllem  26351  usgrexmpl  26354  griedg0prc  26355  cplgr0  26531  usgrexilem  26546  cffldtocusgr  26553  rgrusgrprc  26695  rusgrprc  26696  rgrprcx  26698  rgrx0ndm  26699  usgr2pthlem  26869  pthdlem2  26874  uspgrn2crct  26911  wwlksnext  27011  wwlksnfi  27024  disjxwwlkn  27031  clwwlknondisj  27260  clwwlknondisjOLD  27264  0ewlk  27266  0wlk  27268  0pth  27277  1pthdlem1  27287  1trld  27294  wlk2v2elem2  27308  wlk2v2e  27309  upgr3v3e3cycl  27332  upgr4cycl4dv4e  27337  dfconngr1  27340  0conngr  27344  konigsbergumgr  27403  2wspmdisj  27491  2clwwlk2clwwlk  27507  numclwwlk3lemOLD  27550  numclwwlk3lemlem  27551  numclwwlk3lem  27552  ex-dif  27591  ex-in  27593  ex-eprel  27601  ex-id  27602  ex-fl  27615  ex-mod  27617  ex-hash  27621  avril1  27630  2bornot2b  27631  0vfval  27770  vsfval  27797  ajmoi  28023  ajfuni  28024  normlem2  28277  norm3adifii  28314  hhip  28343  hlim0  28401  hlimcaui  28402  hlimf  28403  hhssnv  28430  shscli  28485  shsval2i  28555  h1de2i  28721  fh3i  28791  fh4i  28792  cm2mi  28794  qlaxr3i  28804  mayetes3i  28897  ho0f  28919  hoif  28922  hodidi  28955  ho0subi  28963  hosd1i  28990  adjmo  29000  nmopsetn0  29033  nmfnsetn0  29046  funadj  29054  funcnvadj  29061  nmcexi  29194  cnlnadjlem8  29242  nmoptri2i  29267  opsqrlem4  29311  hmopidmchi  29319  pjoci  29348  pjinvari  29359  abrexdomjm  29652  elim2ifim  29671  iundisj2f  29710  rinvf1o  29741  funcnvmptOLD  29776  dfcnv2  29785  snct  29800  fpwrelmap  29817  fzodif2  29861  iundisj2fi  29865  dp2lt10  29900  dp2ltc  29903  dplti  29922  dpgti  29923  dpexpp1  29925  gsumle  30088  xrge0slmod  30153  xrge0pluscn  30295  zlmds  30317  zlmtset  30318  qqhre  30373  esumrnmpt2  30439  esumfsup  30441  esumpcvgval  30449  hasheuni  30456  esumcvg  30457  esumcvgsum  30459  esumsup  30460  esum2d  30464  dmsigagen  30516  ldgenpisyslem3  30537  measvuni  30586  voliune  30601  volfiniune  30602  br2base  30640  dya2iocuni  30654  eulerpartlem1  30738  eulerpartlemt  30742  eulerpartgbij  30743  fib0  30770  coinfliprv  30853  ballotlem2  30859  ballotlemic  30877  ballotlem7  30906  ballotth  30908  plymul02  30932  rpsqrtcn  30980  chtvalz  31016  circlemethnat  31028  circlevma  31029  circlemethhgt  31030  hgt750lem  31038  bnj226  31109  bnj1101  31162  bnj110  31235  bnj149  31252  bnj150  31253  bnj151  31254  bnj517  31262  bnj580  31290  bnj865  31300  bnj900  31306  bnj996  31332  bnj1110  31357  bnj1133  31364  bnj1128  31365  bnj1145  31368  bnj1137  31370  bnj1171  31375  bnj1176  31380  subfacp1lem5  31473  subfacp1lem6  31474  kur14lem9  31503  cvmcov2  31564  cvmliftlem1  31574  cvmliftlem4  31577  cvmliftlem5  31578  msrfo  31750  problem5  31870  brtpid1  31909  brtpid2  31910  brtpid3  31911  logi  31927  faclimlem1  31936  domep  32003  axextndbi  32015  poseq  32059  frrlem6  32095  frrlem10  32097  sltval2  32115  noxp1o  32122  nosepnelem  32136  txprel  32292  relsset  32301  relbigcup  32310  fvbigcup  32315  fnsingle  32332  fvsingle  32333  snelsingles  32335  funimage  32341  fullfunfnv  32359  imagesset  32366  funtransport  32444  colinrel  32470  funray  32553  funline  32555  0hf  32590  neibastop2lem  32661  filnetlem3  32681  waj-ax  32719  lukshef-ax2  32720  arg-ax  32721  limsucncmpi  32750  dnizeq0  32771  knoppcnlem8  32796  knoppcnlem11  32799  cnndvlem1  32834  bj-babylob  32895  bj-ax12ssb  32941  bj-dvdemo1  33108  bj-disjcsn  33242  bj-snsetex  33257  bj-0eltag  33272  bj-2upln0  33317  bj-2upln1upl  33318  f1omptsnlem  33494  f1omptsn  33495  icoreresf  33511  relowlssretop  33522  relowlpssretop  33523  cnfinltrel  33552  pigt3  33715  matunitlindf  33720  poimirlem3  33725  poimirlem9  33731  poimirlem16  33738  poimirlem17  33739  poimirlem18  33740  poimirlem19  33741  poimirlem20  33742  poimirlem26  33748  mblfinlem1  33759  mblfinlem2  33760  ismblfin  33763  voliunnfl  33766  cnambfre  33771  cover2  33821  abrexdom  33838  fdc  33854  cncfres  33877  heibor1lem  33921  grposnOLD  33994  bicontr  34192  an12i  34213  tsim1  34250  ac6s6f  34294  vvdifopab  34348  opabf  34453  xrnrel  34458  relcoels  34502  cnvcosseq  34515  refrelcoss3  34536  refrelcoss2  34537  symrelcoss2  34539  refrelcoss  34595  symrelcoss  34629  ax13fromc9  34695  dedths  34751  renegclALT  34752  hlhilslem  37732  moxfr  37757  mapfzcons1  37782  diophrw  37824  0dioph  37844  vdioph  37845  rabren3dioph  37881  2nn0ind  38012  rpnnen3  38101  kelac2lem  38136  frlmpwfi  38170  ifpbiidcor2  38330  relintabex  38389  eliunov2  38473  xphe  38577  0he  38578  he0  38580  snhesn  38582  idhe  38583  frege54cor1c  38711  clsk1independent  38846  neicvgnvor  38916  amgm2d  39003  amgm3d  39004  amgm4d  39005  lhe4.4ex1a  39030  rusbcALT  39142  ipo0  39155  ifr0  39156  vk15.4j  39236  2sb5nd  39278  dfvd1ir  39291  dfvd2anir  39302  dfvd2ir  39304  dfvd3ir  39311  dfvd3anir  39314  iden2  39341  e0bir  39506  uun2221p1  39543  uun2221p2  39544  2sb5ndVD  39645  2sb5ndALT  39667  iunconnlem2  39670  fnchoice  39687  unisn0  39721  eliincex  39792  icof  39910  mptssid  39949  supminfxr  40192  fsumiunss  40310  climlimsupcex  40504  liminfltlimsupex  40516  liminflelimsupcex  40532  xlimrel  40549  resincncf  40591  dvnprodlem3  40666  mbf0  40676  volioc  40691  volico  40703  dmvolss  40705  volioof  40707  stoweidlem13  40733  stoweidlem34  40754  stirlinglem5  40798  stirlinglem13  40806  stirlingr  40810  fourierdlem42  40869  fourierdlem62  40888  fouriersw  40951  etransc  41003  salexct  41055  salexct2  41060  salgencntex  41064  sge0rnn0  41088  gsumge0cl  41091  sge00  41096  sge0resplit  41126  sge0reuz  41167  omeiunle  41237  0ome  41249  icoresmbl  41263  ovn0lem  41285  ovnhoilem1  41321  hspmbl  41349  ovolval5lem3  41374  nsssmfmbf  41493  mbfpsssmf  41497  smfresal  41501  smfmullem4  41507  smfpimbor1lem1  41511  smfpimbor1lem2  41512  aistia  41570  aisfina  41571  aiffnbandciffatnotciffb  41577  axorbciffatcxorb  41578  abnotbtaxb  41588  abnotataxb  41589  pfx2  41922  m3prm  42016  m7prm  42026  0noddALTV  42110  2noddALTV  42114  sbgoldbo  42185  nnsum3primes4  42186  evengpop3  42196  spr0nelg  42236  oddinmgm  42325  2zrngamgm  42449  2zrngaabl  42454  2zrngmmgm  42456  2zrngnring  42462  fldhmsubc  42594  fldhmsubcALTV  42612  eliunxp2  42622  zlmodzxzldeplem  42797  zlmodzxzldep  42803  ldepslinc  42808  ex-gte  42983  empty-surprise  43041  eximp-surprise2  43044  amgmw2d  43063
  Copyright terms: Public domain W3C validator