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

Theorem mpbi 220
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 11-May-1993.)
Hypotheses
Ref Expression
mpbi.min 𝜑
mpbi.maj (𝜑𝜓)
Assertion
Ref Expression
mpbi 𝜓

Proof of Theorem mpbi
StepHypRef Expression
1 mpbi.min . 2 𝜑
2 mpbi.maj . . 3 (𝜑𝜓)
32biimpi 206 . 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.74i  260  notbii  309  pm5.19  374  ori  389  imori  428  pm4.71i  667  pm4.71ri  668  pm5.32i  672  pm3.24  962  pm5.16  970  biluk  1012  4exmidOLD  1040  dn1  1046  3ori  1533  cadan  1693  nic-dfim  1739  nic-dfneg  1740  nic-mp  1741  nic-mpALT  1742  tbw-negdf  1769  rb-imdf  1820  nfri  1860  mpgbi  1870  19.35i  1951  19.36ivOLD  2066  19.37ivOLD  2072  nfim1  2210  19.36i  2242  ax6  2392  sbie  2541  axi12  2734  bm1.1  2741  eqcomi  2765  eqtri  2778  eleqtri  2833  neii  2930  necomi  2982  neeqtri  3000  neli  3033  nrex  3134  rexlimi  3158  rexlimiv  3161  isseti  3345  vtocl2  3397  vtocl3  3398  eueq1  3516  euxfr2  3528  cdeqri  3558  sseqtri  3774  3sstr3i  3780  pssn2lp  3846  equncomi  3898  unssi  3927  ssini  3975  unabs  3993  inabs  3994  dfin4  4006  difid  4087  ab0orv  4092  npss0OLD  4154  disjdif  4180  difin0  4181  snid  4349  rabrsn  4399  iinrab2  4731  symdifv  4746  rintn0  4767  breqtri  4825  axsep  4928  bm1.3ii  4932  ax6vsep  4933  zfnuleu  4934  notzfaus  4985  zfpow  4989  dtru  5002  reusv2lem4  5017  reuxfr2d  5036  dtruALT  5044  dtruALT2  5056  op1stb  5084  copsexg  5100  uniop  5121  pwundif  5167  rn0  5528  dmresi  5611  issref  5663  somincom  5684  cnvcnv  5740  cnvcnvOLD  5741  rescnvcnv  5751  cnvcnvres  5752  cnvsnOLD  5775  cocnvcnv2  5804  cores2  5805  co01  5807  cnviin  5829  onunisuci  5998  iota4an  6027  fnopab  6175  mpt0  6178  fnmpti  6179  f1cnvcnv  6266  f1ovi  6332  eliman0  6380  fvco4i  6434  fmpti  6542  fvsnun2  6609  funiunfv  6665  oprabss  6907  relmptopab  7044  zfun  7111  tfinds2  7224  omon  7237  2nd0  7336  f1stres  7353  f2ndres  7354  cnvoprab  7393  relmpt2opab  7423  df1st2  7427  df2nd2  7428  fsplit  7446  reldmtpos  7525  dftpos4  7536  tpostpos  7537  tpos0  7547  wfrlem4  7583  smo0  7620  tfrlem14  7652  tfrlem16  7654  rdgsucg  7684  rdglimg  7686  frfnom  7695  oawordeulem  7799  uniixp  8093  dfdom2  8143  ssdomg  8163  xpcomf1o  8210  sbthlem5  8235  pwdom  8273  limensuci  8297  fiint  8398  fidomdm  8404  residfi  8408  pwfilem  8421  mptfi  8426  fisn  8494  dffi3  8498  ordtypelem6  8589  ordtypelem7  8590  wemaplem2  8613  wdompwdom  8644  harwdom  8656  suc11reg  8685  zfinf  8705  axinf2  8706  noinfep  8726  cantnfvalf  8731  cantnflt  8738  cantnf0  8741  cantnf  8759  tz9.1c  8775  tc2  8787  r111  8807  r1tr2  8809  r1ordg  8810  r1sssuc  8815  r1val1  8818  tz9.13  8823  r1elssi  8837  pwwf  8839  rankopb  8884  rankeq0b  8892  ranksuc  8897  rankmapu  8910  rankxplim  8911  rankxplim3  8913  rankxpsuc  8914  cp  8923  karden  8927  card0  8970  cardlim  8984  cardom  8998  infxpenlem  9022  alephsuc2  9089  alephgeom  9091  unialeph  9110  dfac4  9131  dfacacn  9151  cda1dif  9186  pm110.643  9187  infcda1  9203  ackbij1lem13  9242  ackbij2  9253  cf0  9261  cfsuc  9267  cfom  9274  cfslb2n  9278  ominf4  9322  fin23lem17  9348  fin23lem28  9350  fin23lem30  9352  fin23lem31  9353  fin23lem40  9361  isfin1-3  9396  dfacfin7  9409  fin1a2lem6  9415  itunitc1  9430  axcc3  9448  dcomex  9457  axdc2lem  9458  axcclem  9467  zfac  9470  ac3  9472  ackm  9475  axac2  9476  axac  9477  axaci  9478  cardeqv  9479  numth2  9481  numth  9482  dmct  9534  brdom3  9538  fin71ac  9543  cardf  9560  aleph1  9581  cfpwsdom  9594  smobeth  9596  zfcndrep  9624  zfcndpow  9626  zfcndac  9629  gch2  9685  wunex3  9751  tskpr  9780  inar1  9785  rankcf  9787  tskcard  9791  tskuni  9793  grothpw  9836  axgroth4  9842  grothprim  9844  inaprc  9846  dmaddpi  9900  dmmulpi  9901  1lt2pi  9915  addpqf  9954  mulpqf  9956  1lt2nq  9983  supsrlem  10120  ssxr  10295  gtso  10307  subf  10471  negne0i  10544  mulnzcnopr  10861  infrenegsup  11194  halflt1  11438  nn0ssz  11586  3halfnz  11644  zeo  11651  numlt  11715  numltc  11716  le9lt10  11717  decle  11728  decleOLD  11731  declecOLD  11732  uzf  11878  zgt1rpn0n1  12060  xaddf  12244  xsubge0  12280  xmulf  12291  ixxf  12374  ixxssxr  12376  iooval2  12397  ioof  12460  unirnioo  12462  dfioo2  12463  xrge0neqmnf  12465  fzval2  12518  fzf  12519  0nelfz1  12549  fz10  12551  fzpreddisj  12579  4fvwrd4  12649  fzof  12657  fzo0  12682  fldiv4p1lem1div2  12826  fldiv4lem1div2  12828  om2uzoi  12944  faclbnd4lem1  13270  hashkf  13309  hashgval  13310  hashinf  13312  hashresfn  13318  hashnn0n0nn  13368  hashbclem  13424  hashge3el3dif  13456  wrdexg  13497  rev0  13709  f1oun2prg  13858  trclublem  13931  sqrt2gt1lt2  14210  limsupgord  14398  fclim  14479  fsumrelem  14734  ackbijnn  14755  incexclem  14763  incexc  14764  arisum2  14788  georeclim  14798  geoisumr  14804  0.999...  14807  0.999...OLD  14808  geoihalfsum  14809  risefall0lem  14952  ege2le3  15015  sin0  15074  ef01bndlem  15109  cos2bnd  15113  cos01gt0  15116  sincos2sgn  15119  sin4lt0  15120  rpnnen2lem3  15140  rpnnen2lem9  15146  rexpen  15152  cnso  15171  dvdslelem  15229  n2dvds1  15302  divalglem1  15315  divalglem5  15318  divalglem6  15319  divalglem10  15323  flodddiv4  15335  0bits  15359  sadcf  15373  sadcadd  15378  bitsshft  15395  smupf  15398  gcdf  15432  eucalgf  15494  2prm  15603  dfphi2  15677  pockthi  15809  prmrec  15824  vdwapf  15874  vdwap0  15878  vdwlem6  15888  karatsuba  15990  karatsubaOLD  15991  1259lem5  16040  2503lem3  16044  4001lem4  16049  structcnvcnv  16069  structfn  16072  strlemor1OLD  16167  strleun  16170  prdsval  16313  prdsds  16322  imasvscafn  16395  xpsc0  16418  xpsc1  16419  xpsff1o  16426  sscpwex  16672  wunfunc  16756  wunnat  16813  eldmcoa  16912  coapm  16918  catcfuccl  16956  catcxpccl  17044  yonedainv  17118  plusffval  17444  grpinvfvi  17660  mulgfvi  17742  symgsssg  18083  symgfisg  18084  psgnunilem5  18110  sylow3lem2  18239  oppglsm  18253  efgmf  18322  efgval  18326  efgsf  18338  0frgp  18388  dmdprd  18593  dprdval  18598  invrfval  18869  drngui  18951  scaffval  19079  rmodislmod  19129  lssintcl  19162  mplsubrglem  19637  opsrtoslem2  19683  cnfldfun  19956  cnfld0  19968  cnfld1  19969  cnfldsub  19972  xrsds  19987  psgnghm  20124  zrhpsgnmhm  20128  recrng  20165  ipffval  20191  ocv1  20221  dsmmbas2  20279  mdetralt  20612  maducoeval2  20644  eltpsi  20946  unitg  20969  fctop  21006  cctop  21008  ppttop  21009  epttop  21011  leordtvallem1  21212  leordtvallem2  21213  iccordt  21216  iscnp2  21241  discmp  21399  conncompcld  21435  1stcrestlem  21453  2ndcdisj  21457  topnlly  21492  disllycmp  21499  dis1stc  21500  txuni2  21566  xkotf  21586  dfac14lem  21618  prdstps  21630  txindis  21635  tx1stc  21651  xkohaus  21654  xkoptsub  21655  cnmpt1st  21669  cnmpt2nd  21670  ptcmpfi  21814  trfil1  21887  fin1aufil  21933  tgpconncompeqg  22112  tgpconncomp  22113  tsmsres  22144  trust  22230  met1stc  22523  dscmet  22574  retopon  22764  cnfldtopon  22783  xrsxmet  22809  xrsmopn  22812  iimulcn  22934  icopnfhmeo  22939  iccpnfhmeo  22941  xrhmeo  22942  cnheiborlem  22950  lebnumii  22962  ishtpy  22968  htpycc  22976  pco1  23011  pcohtpylem  23015  pcopt  23018  pcopt2  23019  pcoass  23020  pcorevlem  23022  cfilresi  23289  rrxcph  23376  ovoliunlem3  23468  ovolicc1  23480  ovolicc2  23486  volf  23493  ioorf  23537  dyadf  23555  dyadmbl  23564  vitalilem5  23576  vitali  23577  mbfimaopnlem  23617  mbflimsup  23628  0plef  23634  i1fima  23640  i1fima2  23641  i1fd  23643  itg1ge0  23648  itg10  23650  i1f1lem  23651  i1fadd  23657  i1fmul  23658  i1fmulc  23665  mbfi1fseqlem5  23681  itg2addlem  23720  reldv  23829  dvbsss  23861  dvef  23938  lhop1lem  23971  deg1fvi  24040  plypf1  24163  coeeulem  24175  coeeu  24176  vieta1lem2  24261  aannenlem3  24280  aalioulem3  24284  dvradcnv  24370  pserulm  24371  pserdvlem2  24377  abelthlem6  24385  sinhalfpilem  24410  sincos4thpi  24460  tan4thpi  24461  sincos6thpi  24462  pige3  24464  resinf1o  24477  tanord1  24478  tanregt0  24480  efabl  24491  relogrn  24503  dfrelog  24507  logneg  24529  logltb  24541  logcn  24588  logf1o2  24591  dvlog  24592  efopnlem2  24598  efopn  24599  logccv  24604  dvsqrt  24678  dvcnsqrt  24680  cxpcn3  24684  logblog  24725  angpined  24752  1cubr  24764  asinsin  24814  asin1  24816  reasinsin  24818  atan0  24830  atanbnd  24848  atan1  24850  log2cnv  24866  log2ub  24871  log2le1  24872  birthday  24876  amgmlem  24911  emcllem5  24921  emgt0  24928  harmonicbnd3  24929  ftalem3  24996  basellem4  25005  sgmf  25066  ppi1  25085  cht1  25086  vma1  25087  ppiltx  25098  sqff1o  25103  ppiublem1  25122  ppiublem2  25123  ppiub  25124  chtub  25132  dchreq  25178  bposlem7  25210  bposlem8  25211  bposlem9  25212  lgsdir2lem2  25246  lgsdir2lem3  25247  chebbnd1  25356  chto1ub  25360  chpo1ubb  25365  pntibndlem1  25473  tgldimor  25592  tglnfn  25637  axlowdimlem4  26020  axlowdimlem16  26032  axlowdim  26036  upgrfi  26181  lfgrnloop  26215  lfuhgr1v0e  26341  usgrexmplef  26346  usgrres  26395  vdegp1bi  26639  vtxdginducedm1lem2  26642  pthdlem2  26870  wpthswwlks2on  27078  0ewlk  27262  0pth  27273  konigsbergiedgw  27396  konigsberglem1  27400  konigsberglem2  27401  konigsberglem3  27402  konigsberglem4  27403  konigsberglem5  27404  ex-dif  27587  ex-un  27588  ex-in  27589  ex-fl  27611  avril1  27626  n0lplig  27642  vcex  27738  cnidOLD  27742  cnnvm  27842  ipasslem8  27997  ipasslem10  27999  hvsubf  28177  normlem1  28272  normlem6  28277  normlem7  28278  norm-ii-i  28299  norm3adifii  28310  hilid  28323  hlimf  28399  hhssabloi  28424  hhssnv  28426  hhshsslem1  28429  shincli  28526  shsval2i  28551  shs0i  28613  chj0i  28619  chm1i  28620  chincli  28624  chdmm1i  28641  shjshsi  28656  chsup0  28712  h1de2bi  28718  spansnpji  28742  cmcmlem  28755  cmcmii  28761  cmcm2ii  28762  cmcm3ii  28763  pjidmi  28837  pjssmii  28845  pj0i  28857  pjocini  28862  mayetes3i  28893  df0op2  28916  hoaddcomi  28936  hoaddassi  28940  hocadddiri  28943  hocsubdiri  28944  hoaddid1i  28950  ho0coi  28952  hoid1i  28953  hoid1ri  28954  hodseqi  28958  honegsubi  28960  adj1o  29058  hoddii  29153  lnopunilem1  29174  lnopunilem2  29175  nmcopexi  29191  nmcopex  29193  nmcoplb  29194  nmcfnexi  29215  nmcfnex  29217  nmcfnlb  29218  adjbd1o  29249  adjcoi  29264  nmopcoadji  29265  opsqrlem6  29309  pjsdii  29319  pjddii  29320  pjidmcoi  29341  pjtoi  29343  pjin1i  29356  pjclem1  29359  stji1i  29406  reuxfr3d  29633  inindif  29656  iuninc  29682  fnresin  29735  rinvf1o  29737  suppss2f  29744  xppreima  29754  ofoprabco  29769  funcnvmptOLD  29772  gtiso  29783  df1stres  29786  df2ndres  29787  snct  29796  padct  29802  ffsrn  29809  fpwrelmapffs  29814  nnindf  29870  nn0min  29872  dp2lt  29897  dp2ltsuc  29898  dp2ltc  29899  dplti  29918  dpmul  29926  dpmul4  29927  ressplusf  29955  xrsclat  29985  xrge0base  29990  xrge00  29991  xrnarchi  30043  xrge0slmod  30149  locfinreflem  30212  locfinref  30213  unicls  30254  sqsscirc1  30259  mhmhmeotmd  30278  rmulccn  30279  raddcn  30280  xrge0iifiso  30286  xrge0iifhmeo  30287  lmxrge0  30303  cnzh  30319  rezh  30320  qqh0  30333  qqh1  30334  qqhre  30369  rrhre  30370  esumnul  30415  esum0  30416  esumsnf  30431  esumpfinvallem  30441  esumpfinvalf  30443  esumpcvgval  30445  esumcvgsum  30455  esumsup  30456  esumcvgre  30458  sigaclfu2  30489  dmsigagen  30512  ldgenpisyslem1  30531  ddemeas  30604  imambfm  30629  mbfmvolf  30633  br2base  30636  omssubadd  30667  sibfof  30707  sitg0  30713  eulerpartlemt  30738  eulerpartgbij  30739  0rrv  30818  coinfliplem  30845  coinflipprob  30846  coinfliprv  30849  ballotlem2  30855  ballotlem4  30865  ballotlem5  30866  ballotlemi1  30869  ballotlem7  30902  ballotth  30904  signsplypnf  30932  signsply0  30933  signsw0g  30938  signswch  30943  signsvf0  30962  hashreprin  31003  reprfz1  31007  chtvalz  31012  hgt750lemd  31031  hgt750lem  31034  hgt750lem2  31035  bnj521  31108  bnj1098  31157  bnj1109  31160  bnj1131  31161  bnj1533  31225  bnj151  31250  bnj580  31286  bnj852  31294  bnj864  31295  bnj865  31296  bnj978  31322  bnj1021  31337  bnj907  31338  bnj1093  31351  bnj1145  31364  bnj1172  31372  bnj1174  31374  bnj1176  31376  bnj1186  31378  subfacf  31460  subfacp1lem1  31464  subfacp1lem5  31469  subfacp1lem6  31470  subfacval3  31474  erdszelem2  31477  kur14lem4  31494  ioosconn  31532  iccllysconn  31535  msrfo  31746  mthmpps  31782  problem5  31866  quad3  31867  circum  31871  axextprim  31881  axrepprim  31882  axunprim  31883  axinfprim  31886  axacprim  31887  inffzOLD  31918  logi  31923  bcneg1  31925  setinds  31984  dfon2lem2  31990  dfon2lem4  31992  axextdfeq  32004  poseq  32055  frrlem4  32085  nosgnn0  32113  sltsolem1  32128  bdayfo  32130  nolt02o  32147  noetalem3  32167  dmscut  32220  fobigcup  32309  snelsingles  32331  fullfunfnv  32355  fullfunfv  32356  rankaltopb  32388  rank0  32579  rankeq1o  32580  hfuni  32593  fneer  32650  neibastop1  32656  nabi1i  32693  nabi2i  32694  limsucncmpi  32746  knoppcnlem8  32792  knoppcnlem11  32795  cnndvlem1  32830  bj-consensusALT  32865  bj-axsep  33095  bj-zfpow  33097  bj-dtru  33099  bj-sbidmOLD  33133  bj-n0i  33237  bj-snsetex  33253  bj-tagss  33270  bj-2upln0  33313  bj-2upln1upl  33314  bj-nuliota  33321  bj-0int  33357  bj-elid  33392  bj-pinftyccb  33415  bj-minftyccb  33419  bj-pinftynminfty  33421  f1omptsnlem  33490  mptsnunlem  33492  topdifinffinlem  33502  relowlpssretop  33519  1oequni2o  33523  cnfinltrel  33548  imadifss  33693  tan2h  33710  poimirlem3  33721  poimirlem9  33727  poimirlem16  33734  poimirlem17  33735  poimirlem18  33736  poimirlem19  33737  poimirlem20  33738  poimirlem22  33740  poimirlem30  33748  mblfinlem1  33755  mblfinlem2  33756  ovoliunnfl  33760  voliunnfl  33762  itg2addnclem  33770  itg2addnclem2  33771  asindmre  33804  areacirclem1  33809  fdc  33850  cntotbnd  33904  heiborlem6  33924  rrnval  33935  reheibor  33947  rngosn3  34032  ineqcomi  34328  cnvresrn  34435  moantr  34446  inxp2  34448  dfxrn2  34457  cnvcosseq  34511  refrelcosslem  34531  1cosscnvxrn  34544  prter2  34666  renegclALT  34748  mapdunirnN  37437  rntrclfvOAI  37752  diophrw  37820  rabren3dioph  37877  pellexlem6  37896  pellex  37897  frmx  37976  frmy  37977  jm2.23  38061  jm2.27dlem3  38076  axac10  38098  pw2f1ocnv  38102  kelac2lem  38132  lmhmlnmsplit  38155  pwfi2f1o  38164  frlmpwfi  38166  ifpbiidcor  38317  cnvnonrel  38392  rnnonrel  38395  resnonrel  38396  cononrel1  38398  cononrel2  38399  fvnonrel  38401  cnvcnvintabd  38404  cnvintabd  38407  rclexi  38420  rtrclex  38422  clcnvlem  38428  cnvrcl0  38430  dmtrcl  38432  rntrcl  38433  dfrtrcl5  38434  iunrelexp0  38492  dmtrclfvRP  38520  rntrclfv  38522  corcltrcl  38529  cotrclrcl  38532  0heALT  38575  frege54cor1a  38656  dssmapnvod  38812  uneqsn  38819  clsk3nimkb  38836  gneispace  38930  int-sqdefd  38982  int-sqgeq0d  38987  seff  39006  expgrowthi  39030  expgrowth  39032  binomcxplemnotnn0  39053  ee233  39223  ax6e2nd  39272  in1  39285  dfvd2ani  39297  dfvd2i  39299  dfvd3i  39306  dfvd3ani  39309  e0bi  39501  uun2221  39538  uun2221p1  39539  uun2221p2  39540  en3lpVD  39575  relopabVD  39632  ax6e2ndVD  39639  ax6e2ndALT  39661  pssnssi  39778  nnf1oxpnn  39879  icof  39906  negpilt0  39987  xrgtso  40055  supxrleubrnmptf  40174  xrpnf  40210  ioontr  40235  iccdifioo  40240  iccdifprioo  40241  uzinico2  40288  fsummulc1f  40301  fsumiunss  40306  fnlimfvre2  40408  limsupreuz  40468  limsupvaluz2  40469  limsup10ex  40504  icccncfext  40599  dvcosre  40625  dvsinax  40626  ioodvbdlimc1lem2  40646  ioodvbdlimc2lem  40648  dvmptmulf  40651  dvnmul  40657  dvmptfprodlem  40658  dvnprodlem2  40661  stoweidlem1  40717  stoweidlem26  40742  stoweidlem34  40750  stoweidlem44  40760  stoweid  40779  stirlinglem5  40794  dirkercncflem1  40819  fourierdlem44  40867  fourierdlem56  40878  fourierdlem62  40884  fourierdlem89  40911  fourierdlem91  40913  fourierdlem100  40922  fourierdlem102  40924  fourierdlem103  40925  fourierdlem104  40926  fourierdlem108  40930  fourierdlem112  40934  fourierdlem114  40936  fouriersw  40947  rrndistlt  41009  gsumge0cl  41087  sge0tsms  41096  sge0ltfirpmpt2  41142  ovn0  41282  hoidmv1le  41310  hoidmvle  41316  ovnsubadd2lem  41361  ovolval4lem1  41365  vonioolem2  41397  smflimlem3  41483  nsssmfmbf  41489  axorbtnotaiffb  41572  axorbciffatcxorb  41574  abnotbtaxb  41584  fmtnoinf  41954  1nevenALTV  42108  nnsum3primes4  42182  tgblthelfgott  42209  tgoldbachlt  42210  tgblthelfgottOLD  42215  tgoldbachltOLD  42216  sprval  42235  ldepslinc  42804  alimp-no-surprise  43036  aacllem  43056  amgmwlem  43057  amgmlemALT  43058
  Copyright terms: Public domain W3C validator