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  310  pm5.19  375  ori  390  imori  429  pm4.71i  663  pm4.71ri  664  pm5.32i  668  pm3.24  925  pm5.16  933  biluk  973  4exmidOLD  997  dn1  1007  3ori  1385  cadan  1545  nic-dfim  1591  nic-dfneg  1592  nic-mp  1593  nic-mpALT  1594  tbw-negdf  1621  rb-imdf  1672  nfri  1712  mpgbi  1722  19.35i  1803  19.36iv  1902  19.37iv  1908  nfim1  2065  19.36i  2097  ax6  2250  sbie  2407  axi12  2599  bm1.1  2606  eqcomi  2630  eqtri  2643  eleqtri  2696  neii  2792  necomi  2844  neeqtri  2862  neli  2895  nrex  2996  rexlimi  3019  rexlimiv  3022  isseti  3199  vtocl2  3251  vtocl3  3252  eueq1  3366  euxfr2  3378  cdeqri  3408  sseqtri  3622  3sstr3i  3628  pssn2lp  3692  equncomi  3743  unssi  3772  ssini  3820  unabs  3838  inabs  3839  dfin4  3849  difid  3928  ab0orv  3933  npss0OLD  3993  disjdif  4018  difin0  4019  snid  4186  rabrsn  4236  iinrab2  4556  symdifv  4571  rintn0  4592  breqtri  4648  axsep  4750  bm1.3ii  4754  ax6vsep  4755  zfnuleu  4756  notzfaus  4810  zfpow  4814  dtru  4827  reusv2lem4  4842  reuxfr2d  4861  dtruALT  4870  dtruALT2  4882  op1stb  4911  copsexg  4926  uniop  4947  pwundif  4991  rn0  5347  dmresi  5426  issref  5478  somincom  5499  cnvcnv  5555  cnvcnvOLD  5556  rescnvcnv  5566  cnvcnvres  5567  cnvsn  5587  cocnvcnv2  5616  cores2  5617  co01  5619  cnviin  5641  onunisuci  5810  iota4an  5839  fnopab  5985  mpt0  5988  fnmpti  5989  f1cnvcnv  6076  f1ovi  6142  eliman0  6190  fvco4i  6243  fmpti  6349  fvsnun2  6414  funiunfv  6471  oprabss  6711  relmptopab  6848  zfun  6915  tfinds2  7025  omon  7038  2nd0  7135  f1stres  7150  f2ndres  7151  relmpt2opab  7219  df1st2  7223  df2nd2  7224  fsplit  7242  reldmtpos  7320  dftpos4  7331  tpostpos  7332  tpos0  7342  wfrlem4  7378  smo0  7415  tfrlem14  7447  tfrlem16  7449  rdgsucg  7479  rdglimg  7481  frfnom  7490  oawordeulem  7594  uniixp  7891  dfdom2  7941  ssdomg  7961  xpcomf1o  8009  sbthlem5  8034  pwdom  8072  limensuci  8096  fiint  8197  fidomdm  8203  residfi  8207  pwfilem  8220  mptfi  8225  fisn  8293  dffi3  8297  ordtypelem6  8388  ordtypelem7  8389  wemaplem2  8412  wdompwdom  8443  harwdom  8455  suc11reg  8476  zfinf  8496  axinf2  8497  noinfep  8517  cantnfvalf  8522  cantnflt  8529  cantnf0  8532  cantnf  8550  tz9.1c  8566  tc2  8578  r111  8598  r1tr2  8600  r1ordg  8601  r1sssuc  8606  r1val1  8609  tz9.13  8614  r1elssi  8628  pwwf  8630  rankopb  8675  rankeq0b  8683  ranksuc  8688  rankmapu  8701  rankxplim  8702  rankxplim3  8704  rankxpsuc  8705  cp  8714  karden  8718  card0  8744  cardlim  8758  cardom  8772  infxpenlem  8796  alephsuc2  8863  alephgeom  8865  unialeph  8884  dfac4  8905  dfacacn  8923  cda1dif  8958  pm110.643  8959  infcda1  8975  ackbij1lem13  9014  ackbij2  9025  cf0  9033  cfsuc  9039  cfom  9046  cfslb2n  9050  ominf4  9094  fin23lem17  9120  fin23lem28  9122  fin23lem30  9124  fin23lem31  9125  fin23lem40  9133  isfin1-3  9168  dfacfin7  9181  fin1a2lem6  9187  itunitc1  9202  axcc3  9220  dcomex  9229  axdc2lem  9230  axcclem  9239  zfac  9242  ac3  9244  ackm  9247  axac2  9248  axac  9249  axaci  9250  cardeqv  9251  numth2  9253  numth  9254  dmct  9306  brdom3  9310  fin71ac  9315  cardf  9332  aleph1  9353  cfpwsdom  9366  smobeth  9368  zfcndrep  9396  zfcndpow  9398  zfcndac  9401  gch2  9457  wunex3  9523  tskpr  9552  inar1  9557  rankcf  9559  tskcard  9563  tskuni  9565  grothpw  9608  axgroth4  9614  grothprim  9616  inaprc  9618  dmaddpi  9672  dmmulpi  9673  1lt2pi  9687  addpqf  9726  mulpqf  9728  1lt2nq  9755  supsrlem  9892  ssxr  10067  gtso  10079  subf  10243  negne0i  10316  mulnzcnopr  10633  infrenegsup  10966  halflt1  11210  nn0ssz  11358  3halfnz  11416  zeo  11423  numlt  11487  numltc  11488  le9lt10  11489  decle  11500  decleOLD  11503  declecOLD  11504  uzf  11650  zgt1rpn0n1  11831  xaddf  12014  xsubge0  12050  xmulf  12061  ixxf  12143  ixxssxr  12145  iooval2  12166  ioof  12229  unirnioo  12231  dfioo2  12232  xrge0neqmnf  12234  fzval2  12287  fzf  12288  0nelfz1  12318  fz10  12320  fzpreddisj  12348  4fvwrd4  12416  fzof  12424  fzo0  12449  fldiv4p1lem1div2  12592  fldiv4lem1div2  12594  om2uzoi  12710  faclbnd4lem1  13036  hashkf  13075  hashgval  13076  hashinf  13078  hashresfn  13084  hashnn0n0nn  13136  hashbclem  13190  hashge3el3dif  13222  wrdexg  13270  rev0  13466  f1oun2prg  13614  trclublem  13684  sqrt2gt1lt2  13965  limsupgord  14153  fclim  14234  fsumrelem  14485  ackbijnn  14504  incexclem  14512  incexc  14513  arisum2  14537  georeclim  14547  geoisumr  14553  0.999...  14556  0.999...OLD  14557  geoihalfsum  14558  risefall0lem  14701  ege2le3  14764  sin0  14823  ef01bndlem  14858  cos2bnd  14862  cos01gt0  14865  sincos2sgn  14868  sin4lt0  14869  rpnnen2lem3  14889  rpnnen2lem9  14895  rexpen  14901  cnso  14920  dvdslelem  14974  n2dvds1  15047  divalglem1  15060  divalglem5  15063  divalglem6  15064  divalglem10  15068  flodddiv4  15080  0bits  15104  sadcf  15118  sadcadd  15123  bitsshft  15140  smupf  15143  gcdf  15177  eucalgf  15239  2prm  15348  dfphi2  15422  pockthi  15554  prmrec  15569  vdwapf  15619  vdwap0  15623  vdwlem6  15633  karatsuba  15735  karatsubaOLD  15736  1259lem5  15785  2503lem3  15789  4001lem4  15794  structcnvcnv  15813  structfn  15816  strlemor1OLD  15909  strleun  15912  prdsval  16055  prdsds  16064  imasvscafn  16137  xpsc0  16160  xpsc1  16161  xpsff1o  16168  sscpwex  16415  wunfunc  16499  wunnat  16556  eldmcoa  16655  coapm  16661  catcfuccl  16699  catcxpccl  16787  yonedainv  16861  plusffval  17187  grpinvfvi  17403  mulgfvi  17485  symgsssg  17827  symgfisg  17828  psgnunilem5  17854  sylow3lem2  17983  oppglsm  17997  efgmf  18066  efgval  18070  efgsf  18082  0frgp  18132  dmdprd  18337  dprdval  18342  invrfval  18613  drngui  18693  scaffval  18821  rmodislmod  18871  lssintcl  18904  mplsubrglem  19379  opsrtoslem2  19425  cnfldfun  19698  cnfld0  19710  cnfld1  19711  cnfldsub  19714  xrsds  19729  psgnghm  19866  zrhpsgnmhm  19870  recrng  19907  ipffval  19933  ocv1  19963  dsmmbas2  20021  mdetralt  20354  maducoeval2  20386  eltpsi  20688  unitg  20711  fctop  20748  cctop  20750  ppttop  20751  epttop  20753  leordtvallem1  20954  leordtvallem2  20955  iccordt  20958  iscnp2  20983  discmp  21141  conncompcld  21177  1stcrestlem  21195  2ndcdisj  21199  topnlly  21234  disllycmp  21241  dis1stc  21242  txuni2  21308  xkotf  21328  dfac14lem  21360  prdstps  21372  txindis  21377  tx1stc  21393  xkohaus  21396  xkoptsub  21397  cnmpt1st  21411  cnmpt2nd  21412  ptcmpfi  21556  trfil1  21630  fin1aufil  21676  tgpconncompeqg  21855  tgpconncomp  21856  tsmsres  21887  trust  21973  met1stc  22266  dscmet  22317  retopon  22507  cnfldtopon  22526  xrsxmet  22552  xrsmopn  22555  iimulcn  22677  icopnfhmeo  22682  iccpnfhmeo  22684  xrhmeo  22685  cnheiborlem  22693  lebnumii  22705  ishtpy  22711  htpycc  22719  pco1  22755  pcohtpylem  22759  pcopt  22762  pcopt2  22763  pcoass  22764  pcorevlem  22766  cfilresi  23033  rrxcph  23120  ovoliunlem3  23212  ovolicc1  23224  ovolicc2  23230  volf  23237  ioorf  23281  dyadf  23299  dyadmbl  23308  vitalilem5  23321  vitali  23322  mbfimaopnlem  23362  mbflimsup  23373  0plef  23379  i1fima  23385  i1fima2  23386  i1fd  23388  itg1ge0  23393  itg10  23395  i1f1lem  23396  i1fadd  23402  i1fmul  23403  i1fmulc  23410  mbfi1fseqlem5  23426  itg2addlem  23465  reldv  23574  dvbsss  23606  dvef  23681  lhop1lem  23714  deg1fvi  23783  plypf1  23906  coeeulem  23918  coeeu  23919  vieta1lem2  24004  aannenlem3  24023  aalioulem3  24027  dvradcnv  24113  pserulm  24114  pserdvlem2  24120  abelthlem6  24128  sinhalfpilem  24153  sincos4thpi  24203  tan4thpi  24204  sincos6thpi  24205  pige3  24207  resinf1o  24220  tanord1  24221  tanregt0  24223  efabl  24234  relogrn  24246  dfrelog  24250  logneg  24272  logltb  24284  logcn  24327  logf1o2  24330  dvlog  24331  efopnlem2  24337  efopn  24338  logccv  24343  dvsqrt  24417  dvcnsqrt  24419  cxpcn3  24423  logblog  24464  angpined  24491  1cubr  24503  asinsin  24553  asin1  24555  reasinsin  24557  atan0  24569  atanbnd  24587  atan1  24589  log2cnv  24605  log2ub  24610  log2le1  24611  birthday  24615  amgmlem  24650  emcllem5  24660  emgt0  24667  harmonicbnd3  24668  ftalem3  24735  basellem4  24744  sgmf  24805  ppi1  24824  cht1  24825  vma1  24826  ppiltx  24837  sqff1o  24842  ppiublem1  24861  ppiublem2  24862  ppiub  24863  chtub  24871  dchreq  24917  bposlem7  24949  bposlem8  24950  bposlem9  24951  lgsdir2lem2  24985  lgsdir2lem3  24986  chebbnd1  25095  chto1ub  25099  chpo1ubb  25104  pntibndlem1  25212  tgldimor  25331  tglnfn  25376  axlowdimlem4  25759  axlowdimlem16  25771  axlowdim  25775  upgrfi  25916  lfgrnloop  25949  lfuhgr1v0e  26073  usgrexmplef  26078  vdegp1bi  26353  pthdlem2  26567  0ewlk  26875  0pth  26886  konigsbergiedgw  27008  konigsbergiedgwOLD  27009  konigsberglem1  27014  konigsberglem2  27015  konigsberglem3  27016  konigsberglem4  27017  konigsberglem5  27018  frgrwopreg2  27080  ex-dif  27168  ex-un  27169  ex-in  27170  ex-fl  27192  avril1  27207  n0lplig  27223  vcex  27321  cnidOLD  27325  cnnvm  27425  ipasslem8  27580  ipasslem10  27582  hvsubf  27760  normlem1  27855  normlem6  27860  normlem7  27861  norm-ii-i  27882  norm3adifii  27893  hilid  27906  hlimf  27982  hhssabloi  28007  hhssnv  28009  hhshsslem1  28012  shincli  28109  shsval2i  28134  shs0i  28196  chj0i  28202  chm1i  28203  chincli  28207  chdmm1i  28224  shjshsi  28239  chsup0  28295  h1de2bi  28301  spansnpji  28325  cmcmlem  28338  cmcmii  28344  cmcm2ii  28345  cmcm3ii  28346  pjidmi  28420  pjssmii  28428  pj0i  28440  pjocini  28445  mayetes3i  28476  df0op2  28499  hoaddcomi  28519  hoaddassi  28523  hocadddiri  28526  hocsubdiri  28527  hoaddid1i  28533  ho0coi  28535  hoid1i  28536  hoid1ri  28537  hodseqi  28541  honegsubi  28543  adj1o  28641  hoddii  28736  lnopunilem1  28757  lnopunilem2  28758  nmcopexi  28774  nmcopex  28776  nmcoplb  28777  nmcfnexi  28798  nmcfnex  28800  nmcfnlb  28801  adjbd1o  28832  adjcoi  28847  nmopcoadji  28848  opsqrlem6  28892  pjsdii  28902  pjddii  28903  pjidmcoi  28924  pjtoi  28926  pjin1i  28939  pjclem1  28942  stji1i  28989  reuxfr3d  29218  inindif  29242  iuninc  29265  fnresin  29315  rinvf1o  29317  suppss2f  29322  xppreima  29332  ofoprabco  29348  funcnvmptOLD  29351  gtiso  29362  df1stres  29365  df2ndres  29366  snct  29375  padct  29381  ffsrn  29388  fpwrelmapffs  29393  nnindf  29448  nn0min  29450  ressplusf  29477  xrsclat  29507  xrge0base  29512  xrge00  29513  xrnarchi  29565  xrge0slmod  29671  locfinreflem  29731  locfinref  29732  unicls  29773  sqsscirc1  29778  mhmhmeotmd  29797  rmulccn  29798  raddcn  29799  xrge0iifiso  29805  xrge0iifhmeo  29806  lmxrge0  29822  cnzh  29838  rezh  29839  qqh0  29852  qqh1  29853  qqhre  29888  rrhre  29889  esumnul  29933  esum0  29934  esumsnf  29949  esumpfinvallem  29959  esumpfinvalf  29961  esumpcvgval  29963  esumcvgsum  29973  esumsup  29974  esumcvgre  29976  sigaclfu2  30007  dmsigagen  30030  ldgenpisyslem1  30049  ddemeas  30122  imambfm  30147  mbfmvolf  30151  br2base  30154  omssubadd  30185  sibfof  30225  sitg0  30231  eulerpartlemt  30256  eulerpartgbij  30257  0rrv  30336  coinfliplem  30363  coinflipprob  30364  coinfliprv  30367  ballotlem2  30373  ballotlem4  30383  ballotlem5  30384  ballotlemi1  30387  ballotlem7  30420  ballotth  30422  signsplypnf  30449  signsply0  30450  signsw0g  30455  signswch  30460  signsvf0  30479  bnj521  30566  bnj1098  30615  bnj1109  30618  bnj1131  30619  bnj1533  30683  bnj151  30708  bnj580  30744  bnj852  30752  bnj864  30753  bnj865  30754  bnj978  30780  bnj1021  30795  bnj907  30796  bnj1093  30809  bnj1145  30822  bnj1172  30830  bnj1174  30832  bnj1176  30834  bnj1186  30836  subfacf  30918  subfacp1lem1  30922  subfacp1lem5  30927  subfacp1lem6  30928  subfacval3  30932  erdszelem2  30935  kur14lem4  30952  ioosconn  30990  iccllysconn  30993  msrfo  31204  mthmpps  31240  problem5  31324  quad3  31325  circum  31329  axextprim  31339  axrepprim  31340  axunprim  31341  axinfprim  31344  axacprim  31345  inffzOLD  31376  logi  31381  bcneg1  31383  setinds  31437  dfon2lem2  31443  dfon2lem4  31445  axextdfeq  31457  poseq  31504  frrlem4  31537  nosgnn0  31565  sltsolem1  31581  bdayfo  31591  fobigcup  31702  snelsingles  31724  fullfunfnv  31748  fullfunfv  31749  rankaltopb  31781  rank0  31972  rankeq1o  31973  hfuni  31986  fneer  32043  neibastop1  32049  nabi1i  32086  nabi2i  32087  limsucncmpi  32139  knoppcnlem8  32185  knoppcnlem11  32188  cnndvlem1  32223  bj-consensusALT  32258  bj-axsep  32489  bj-zfpow  32491  bj-dtru  32493  bj-sbieOLD  32528  bj-sbidmOLD  32529  bj-n0i  32635  bj-snsetex  32651  bj-tagss  32668  bj-2upln0  32711  bj-2upln1upl  32712  bj-nuliota  32719  bj-elid  32757  bj-pinftyccb  32780  bj-minftyccb  32784  bj-pinftynminfty  32786  f1omptsnlem  32854  mptsnunlem  32856  topdifinffinlem  32866  relowlpssretop  32883  1oequni2o  32887  imadifss  33055  tan2h  33072  poimirlem3  33083  poimirlem9  33089  poimirlem16  33096  poimirlem17  33097  poimirlem18  33098  poimirlem19  33099  poimirlem20  33100  poimirlem22  33102  poimirlem30  33110  mblfinlem1  33117  mblfinlem2  33118  ovoliunnfl  33122  voliunnfl  33124  itg2addnclem  33132  itg2addnclem2  33133  asindmre  33166  areacirclem1  33171  fdc  33212  cntotbnd  33266  heiborlem6  33286  rrnval  33297  reheibor  33309  rngosn3  33394  prter2  33685  renegclALT  33768  mapdunirnN  36458  rntrclfvOAI  36773  diophrw  36841  rabren3dioph  36898  pellexlem6  36917  pellex  36918  frmx  36997  frmy  36998  jm2.23  37082  jm2.27dlem3  37097  axac10  37119  pw2f1ocnv  37123  kelac2lem  37153  lmhmlnmsplit  37176  pwfi2f1o  37185  frlmpwfi  37187  ifpbiidcor  37339  cnvnonrel  37414  rnnonrel  37417  resnonrel  37418  cononrel1  37420  cononrel2  37421  fvnonrel  37423  cnvcnvintabd  37426  cnvintabd  37429  rclexi  37442  rtrclex  37444  clcnvlem  37450  cnvrcl0  37452  dmtrcl  37454  rntrcl  37455  dfrtrcl5  37456  iunrelexp0  37514  dmtrclfvRP  37542  rntrclfv  37544  corcltrcl  37551  cotrclrcl  37554  0heALT  37598  frege54cor1a  37679  dssmapnvod  37835  uneqsn  37842  clsk3nimkb  37859  gneispace  37953  int-sqdefd  38005  int-sqgeq0d  38010  seff  38029  expgrowthi  38053  expgrowth  38055  binomcxplemnotnn0  38076  ee233  38246  ax6e2nd  38295  in1  38308  dfvd2ani  38320  dfvd2i  38322  dfvd3i  38329  dfvd3ani  38332  e0bi  38524  uun2221  38561  uun2221p1  38562  uun2221p2  38563  en3lpVD  38602  relopabVD  38659  ax6e2ndVD  38666  ax6e2ndALT  38688  pssnssi  38805  nnf1oxpnn  38893  icof  38920  negpilt0  38991  xrgtso  39060  ioontr  39182  iccdifioo  39187  iccdifprioo  39188  uzinico2  39235  fsummulc1f  39238  fsumiunss  39243  fnlimfvre2  39345  limsupreuz  39405  limsupvaluz2  39406  icccncfext  39435  dvcosre  39461  dvsinax  39463  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  dvmptmulf  39489  dvnmul  39495  dvmptfprodlem  39496  dvnprodlem2  39499  stoweidlem1  39555  stoweidlem26  39580  stoweidlem34  39588  stoweidlem44  39598  stoweid  39617  stirlinglem5  39632  dirkercncflem1  39657  fourierdlem44  39705  fourierdlem56  39716  fourierdlem62  39722  fourierdlem89  39749  fourierdlem91  39751  fourierdlem100  39760  fourierdlem102  39762  fourierdlem103  39763  fourierdlem104  39764  fourierdlem108  39768  fourierdlem112  39772  fourierdlem114  39774  fouriersw  39785  rrndistlt  39847  gsumge0cl  39925  sge0tsms  39934  sge0ltfirpmpt2  39980  ovn0  40117  hoidmv1le  40145  hoidmvle  40151  ovnsubadd2lem  40196  ovolval4lem1  40200  vonioolem2  40232  smflimlem3  40318  nsssmfmbf  40324  axorbtnotaiffb  40404  axorbciffatcxorb  40406  abnotbtaxb  40416  fmtnoinf  40777  1nevenALTV  40931  nnsum3primes4  40995  tgblthelfgott  41020  tgoldbachlt  41021  tgblthelfgottOLD  41027  tgoldbachltOLD  41028  sprval  41047  ldepslinc  41616  alimp-no-surprise  41860  aacllem  41880  amgmwlem  41881  amgmlemALT  41882
  Copyright terms: Public domain W3C validator