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

Theorem mpbi 219
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 205 . 2 (𝜑𝜓)
41, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wb 195
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 196
This theorem is referenced by:  pm5.74i  259  notbii  309  pm5.19  374  ori  389  imori  428  pm4.71i  662  pm4.71ri  663  pm5.32i  667  pm3.24  922  pm5.16  930  biluk  970  4exmid  977  dn1  1000  3ori  1380  cadan  1539  nic-dfim  1585  nic-dfneg  1586  nic-mp  1587  nic-mpALT  1588  tbw-negdf  1615  rb-imdf  1666  nfri  1706  mpgbi  1716  19.35i  1795  19.36iv  1892  19.37iv  1898  nfim1  2055  19.36i  2086  ax6  2239  sbie  2396  axi12  2588  bm1.1  2595  eqcomi  2619  eqtri  2632  eleqtri  2686  neii  2784  necomi  2836  neeqtri  2854  neli  2885  nrex  2983  rexlimi  3006  rexlimiv  3009  isseti  3182  vtocl2  3234  vtocl3  3235  eueq1  3346  euxfr2  3358  cdeqri  3388  sseqtri  3600  3sstr3i  3606  pssn2lp  3670  equncomi  3721  unssi  3750  ssini  3798  unabs  3816  inabs  3817  dfin4  3826  difid  3902  ab0orv  3907  npss0OLD  3967  disjdif  3992  difin0  3993  snid  4155  rabrsn  4203  iinrab2  4519  symdifv  4534  rintn0  4552  breqtri  4608  axsep  4708  bm1.3ii  4712  ax6vsep  4713  zfnuleu  4714  notzfaus  4766  zfpow  4770  dtru  4783  reusv2lem4  4798  reuxfr2d  4817  dtruALT  4826  dtruALT2  4838  op1stb  4867  copsexg  4882  uniop  4902  pwundif  4945  rn0  5298  dmresi  5376  issref  5428  somincom  5449  cnvcnv  5505  rescnvcnv  5515  cnvcnvres  5516  cnvsn  5536  cocnvcnv2  5564  cores2  5565  co01  5567  cnviin  5589  onunisuci  5758  iota4an  5787  fnopab  5931  mpt0  5934  fnmpti  5935  f1cnvcnv  6022  f1ovi  6087  eliman0  6133  fvco4i  6186  fmpti  6291  fvsnun2  6354  funiunfv  6410  oprabss  6644  relmptopab  6781  zfun  6848  tfinds2  6955  omon  6968  2nd0  7066  f1stres  7081  f2ndres  7082  relmpt2opab  7146  df1st2  7150  df2nd2  7151  fsplit  7169  reldmtpos  7247  dftpos4  7258  tpostpos  7259  tpos0  7269  wfrlem4  7305  smo0  7342  tfrlem14  7374  tfrlem16  7376  rdgsucg  7406  rdglimg  7408  frfnom  7417  oawordeulem  7521  uniixp  7817  dfdom2  7867  ssdomg  7887  xpcomf1o  7934  sbthlem5  7959  pwdom  7997  limensuci  8021  fiint  8122  fidomdm  8128  pwfilem  8143  mptfi  8148  fisn  8216  dffi3  8220  ordtypelem6  8311  ordtypelem7  8312  wemaplem2  8335  wdompwdom  8366  harwdom  8378  suc11reg  8399  zfinf  8419  axinf2  8420  noinfep  8440  cantnfvalf  8445  cantnflt  8452  cantnf0  8455  cantnf  8473  tz9.1c  8489  tc2  8501  r111  8521  r1tr2  8523  r1ordg  8524  r1sssuc  8529  r1val1  8532  tz9.13  8537  r1elssi  8551  pwwf  8553  rankopb  8598  rankeq0b  8606  ranksuc  8611  rankmapu  8624  rankxplim  8625  rankxplim3  8627  rankxpsuc  8628  cp  8637  karden  8641  card0  8667  cardlim  8681  cardom  8695  infxpenlem  8719  alephsuc2  8786  alephgeom  8788  unialeph  8807  dfac4  8828  dfacacn  8846  cda1dif  8881  pm110.643  8882  infcda1  8898  ackbij1lem13  8937  ackbij2  8948  cf0  8956  cfsuc  8962  cfom  8969  cfslb2n  8973  ominf4  9017  fin23lem17  9043  fin23lem28  9045  fin23lem30  9047  fin23lem31  9048  fin23lem40  9056  isfin1-3  9091  dfacfin7  9104  fin1a2lem6  9110  itunitc1  9125  axcc3  9143  dcomex  9152  axdc2lem  9153  axcclem  9162  zfac  9165  ac3  9167  ackm  9170  axac2  9171  axac  9172  axaci  9173  cardeqv  9174  numth2  9176  numth  9177  brdom3  9231  fin71ac  9236  cardf  9251  aleph1  9272  cfpwsdom  9285  smobeth  9287  zfcndrep  9315  zfcndpow  9317  zfcndac  9320  gch2  9376  wunex3  9442  tskpr  9471  inar1  9476  rankcf  9478  tskcard  9482  tskuni  9484  grothpw  9527  axgroth4  9533  grothprim  9535  inaprc  9537  dmaddpi  9591  dmmulpi  9592  1lt2pi  9606  addpqf  9645  mulpqf  9647  1lt2nq  9674  supsrlem  9811  ssxr  9986  gtso  9998  subf  10162  negne0i  10235  mulnzcnopr  10552  infrenegsup  10883  halflt1  11127  nn0ssz  11275  3halfnz  11332  zeo  11339  numlt  11403  numltc  11404  le9lt10  11405  decle  11416  decleOLD  11419  declecOLD  11420  uzf  11566  zgt1rpn0n1  11747  xaddf  11929  xsubge0  11963  xmulf  11974  ixxf  12056  ixxssxr  12058  iooval2  12079  ioof  12142  unirnioo  12144  dfioo2  12145  xrge0neqmnf  12147  fzval2  12200  fzf  12201  0nelfz1  12231  fz10  12233  fzpreddisj  12260  4fvwrd4  12328  fzof  12336  fzo0  12361  fldiv4p1lem1div2  12498  fldiv4lem1div2  12500  om2uzoi  12616  faclbnd4lem1  12942  hashkf  12981  hashgval  12982  hashinf  12984  hashresfn  12990  hashnn0n0nn  13041  hashbclem  13093  hashge3el3dif  13122  wrdexg  13170  rev0  13364  f1oun2prg  13512  trclublem  13582  sqrt2gt1lt2  13863  limsupgord  14051  fclim  14132  fsumrelem  14380  ackbijnn  14399  incexclem  14407  incexc  14408  arisum2  14432  georeclim  14442  geoisumr  14448  0.999...  14451  0.999...OLD  14452  geoihalfsum  14453  risefall0lem  14596  ege2le3  14659  sin0  14718  ef01bndlem  14753  cos2bnd  14757  cos01gt0  14760  sincos2sgn  14763  sin4lt0  14764  rpnnen2lem3  14784  rpnnen2lem9  14790  rexpen  14796  cnso  14815  dvdslelem  14869  n2dvds1  14942  divalglem1  14955  divalglem5  14958  divalglem6  14959  divalglem10  14963  flodddiv4  14975  0bits  14999  sadcf  15013  sadcadd  15018  bitsshft  15035  smupf  15038  gcdf  15072  eucalgf  15134  2prm  15243  dfphi2  15317  pockthi  15449  prmrec  15464  vdwapf  15514  vdwap0  15518  vdwlem6  15528  karatsuba  15630  karatsubaOLD  15631  1259lem5  15680  2503lem3  15684  4001lem4  15689  structcnvcnv  15706  structfn  15708  strlemor1  15796  strleun  15799  prdsval  15938  prdsds  15947  imasvscafn  16020  xpsc0  16043  xpsc1  16044  xpsff1o  16051  sscpwex  16298  wunfunc  16382  wunnat  16439  eldmcoa  16538  coapm  16544  catcfuccl  16582  catcxpccl  16670  yonedainv  16744  plusffval  17070  grpinvfvi  17286  mulgfvi  17368  symgsssg  17710  symgfisg  17711  psgnunilem5  17737  sylow3lem2  17866  oppglsm  17880  efgmf  17949  efgval  17953  efgsf  17965  0frgp  18015  dmdprd  18220  dprdval  18225  invrfval  18496  drngui  18576  scaffval  18704  lssintcl  18785  mplsubrglem  19260  opsrtoslem2  19306  cnfld0  19589  cnfld1  19590  cnfldsub  19593  xrsds  19608  psgnghm  19745  zrhpsgnmhm  19749  recrng  19786  ipffval  19812  ocv1  19842  dsmmbas2  19900  mdetralt  20233  maducoeval2  20265  eltpsi  20561  unitg  20582  fctop  20618  cctop  20620  ppttop  20621  epttop  20623  leordtvallem1  20824  leordtvallem2  20825  iccordt  20828  iscnp2  20853  discmp  21011  concompcld  21047  1stcrestlem  21065  2ndcdisj  21069  topnlly  21104  disllycmp  21111  dis1stc  21112  txuni2  21178  xkotf  21198  dfac14lem  21230  prdstps  21242  txindis  21247  tx1stc  21263  xkohaus  21266  xkoptsub  21267  cnmpt1st  21281  cnmpt2nd  21282  ptcmpfi  21426  trfil1  21500  fin1aufil  21546  tgpconcompeqg  21725  tgpconcomp  21726  tsmsres  21757  trust  21843  met1stc  22136  dscmet  22187  retopon  22377  cnfldtopon  22396  xrsxmet  22420  xrsmopn  22423  iimulcn  22545  icopnfhmeo  22550  iccpnfhmeo  22552  xrhmeo  22553  cnheiborlem  22561  lebnumii  22573  ishtpy  22579  htpycc  22587  pco1  22623  pcohtpylem  22627  pcopt  22630  pcopt2  22631  pcoass  22632  pcorevlem  22634  cfilresi  22901  rrxcph  22988  ovoliunlem3  23079  ovolicc1  23091  ovolicc2  23097  volf  23104  ioorf  23147  dyadf  23165  dyadmbl  23174  vitalilem5  23187  vitali  23188  mbfimaopnlem  23228  mbflimsup  23239  0plef  23245  i1fima  23251  i1fima2  23252  i1fd  23254  itg1ge0  23259  itg10  23261  i1f1lem  23262  i1fadd  23268  i1fmul  23269  i1fmulc  23276  mbfi1fseqlem5  23292  itg2addlem  23331  reldv  23440  dvbsss  23472  dvef  23547  lhop1lem  23580  deg1fvi  23649  plypf1  23772  coeeulem  23784  coeeu  23785  vieta1lem2  23870  aannenlem3  23889  aalioulem3  23893  dvradcnv  23979  pserulm  23980  pserdvlem2  23986  abelthlem6  23994  sinhalfpilem  24019  sincos4thpi  24069  tan4thpi  24070  sincos6thpi  24071  pige3  24073  resinf1o  24086  tanord1  24087  tanregt0  24089  efabl  24100  relogrn  24112  dfrelog  24116  logneg  24138  logltb  24150  logcn  24193  logf1o2  24196  dvlog  24197  efopnlem2  24203  efopn  24204  logccv  24209  dvsqrt  24283  dvcnsqrt  24285  cxpcn3  24289  logblog  24330  angpined  24357  1cubr  24369  asinsin  24419  asin1  24421  reasinsin  24423  atan0  24435  atanbnd  24453  atan1  24455  log2cnv  24471  log2ub  24476  log2le1  24477  birthday  24481  amgmlem  24516  emcllem5  24526  emgt0  24533  harmonicbnd3  24534  ftalem3  24601  basellem4  24610  sgmf  24671  ppi1  24690  cht1  24691  vma1  24692  ppiltx  24703  sqff1o  24708  ppiublem1  24727  ppiublem2  24728  ppiub  24729  chtub  24737  dchreq  24783  bposlem7  24815  bposlem8  24816  bposlem9  24817  lgsdir2lem2  24851  lgsdir2lem3  24852  chebbnd1  24961  chto1ub  24965  chpo1ubb  24970  pntibndlem1  25078  tgldimor  25197  tglnfn  25242  axlowdimlem4  25625  axlowdimlem16  25637  axlowdim  25641  upgrfi  25758  lfgrnloop  25791  umgrafi  25851  usgraexmplef  25929  usgraexmplc  25933  usgrafilem1  25940  2trllemA  26080  wlkntrllem1  26089  wlkntrllem3  26091  0pth  26100  spthispth  26103  2pthon  26132  2pthon3v  26134  constr3trllem3  26180  constr3pthlem3  26185  konigsberg  26514  frgrawopreg2  26578  ex-dif  26672  ex-un  26673  ex-in  26674  ex-fl  26696  avril1  26711  vcex  26817  cnidOLD  26821  cnnvm  26921  ipasslem8  27076  ipasslem10  27078  hvsubf  27256  normlem1  27351  normlem6  27356  normlem7  27357  norm-ii-i  27378  norm3adifii  27389  hilid  27402  hlimf  27478  hhssabloi  27503  hhssnv  27505  hhshsslem1  27508  shincli  27605  shsval2i  27630  shs0i  27692  chj0i  27698  chm1i  27699  chincli  27703  chdmm1i  27720  shjshsi  27735  chsup0  27791  h1de2bi  27797  spansnpji  27821  cmcmlem  27834  cmcmii  27840  cmcm2ii  27841  cmcm3ii  27842  pjidmi  27916  pjssmii  27924  pj0i  27936  pjocini  27941  mayetes3i  27972  df0op2  27995  hoaddcomi  28015  hoaddassi  28019  hocadddiri  28022  hocsubdiri  28023  hoaddid1i  28029  ho0coi  28031  hoid1i  28032  hoid1ri  28033  hodseqi  28037  honegsubi  28039  adj1o  28137  hoddii  28232  lnopunilem1  28253  lnopunilem2  28254  nmcopexi  28270  nmcopex  28272  nmcoplb  28273  nmcfnexi  28294  nmcfnex  28296  nmcfnlb  28297  adjbd1o  28328  adjcoi  28343  nmopcoadji  28344  opsqrlem6  28388  pjsdii  28398  pjddii  28399  pjidmcoi  28420  pjtoi  28422  pjin1i  28435  pjclem1  28438  stji1i  28485  reuxfr3d  28713  inindif  28738  iuninc  28761  fnresin  28812  rinvf1o  28814  suppss2f  28819  xppreima  28829  ofoprabco  28847  funcnvmptOLD  28850  gtiso  28861  df1stres  28864  df2ndres  28865  snct  28874  dmct  28877  padct  28885  ffsrn  28892  fpwrelmapffs  28897  nnindf  28952  nn0min  28954  ressplusf  28981  xrsclat  29011  xrge0base  29016  xrge00  29017  xrnarchi  29069  xrge0slmod  29175  locfinreflem  29235  locfinref  29236  unicls  29277  sqsscirc1  29282  mhmhmeotmd  29301  rmulccn  29302  raddcn  29303  xrge0iifiso  29309  xrge0iifhmeo  29310  lmxrge0  29326  cnzh  29342  rezh  29343  qqh0  29356  qqh1  29357  qqhre  29392  rrhre  29393  esumnul  29437  esum0  29438  esumsnf  29453  esumpfinvallem  29463  esumpfinvalf  29465  esumpcvgval  29467  esumcvgsum  29477  esumsup  29478  esumcvgre  29480  sigaclfu2  29511  dmsigagen  29534  ldgenpisyslem1  29553  ddemeas  29626  imambfm  29651  mbfmvolf  29655  br2base  29658  omssubadd  29689  sibfof  29729  sitg0  29735  eulerpartlemt  29760  eulerpartgbij  29761  0rrv  29840  coinfliplem  29867  coinflipprob  29868  coinfliprv  29871  ballotlem2  29877  ballotlem4  29887  ballotlem5  29888  ballotlemi1  29891  ballotlem7  29924  ballotth  29926  signsplypnf  29953  signsply0  29954  signsw0g  29959  signswch  29964  signsvf0  29983  bnj521  30059  bnj1098  30108  bnj1109  30111  bnj1131  30112  bnj1533  30176  bnj151  30201  bnj580  30237  bnj852  30245  bnj864  30246  bnj865  30247  bnj978  30273  bnj1021  30288  bnj907  30289  bnj1093  30302  bnj1145  30315  bnj1172  30323  bnj1174  30325  bnj1176  30327  bnj1186  30329  subfacf  30411  subfacp1lem1  30415  subfacp1lem5  30420  subfacp1lem6  30421  subfacval3  30425  erdszelem2  30428  kur14lem4  30445  iooscon  30483  iccllyscon  30486  msrfo  30697  mthmpps  30733  problem5  30817  quad3  30818  circum  30822  axextprim  30832  axrepprim  30833  axunprim  30834  axinfprim  30837  axacprim  30838  inffzOLD  30868  logi  30873  bcneg1  30875  setinds  30927  dfon2lem2  30933  dfon2lem4  30935  axextdfeq  30947  poseq  30994  frrlem4  31027  nosgnn0  31055  sltsolem1  31067  bdayfo  31074  fobigcup  31177  snelsingles  31199  fullfunfnv  31223  fullfunfv  31224  rankaltopb  31256  rank0  31447  rankeq1o  31448  hfuni  31461  fneer  31518  neibastop1  31524  nabi1i  31561  nabi2i  31562  limsucncmpi  31614  knoppcnlem8  31660  knoppcnlem11  31663  cnndvlem1  31698  bj-consensusALT  31733  bj-nfxfr  31794  bj-axsep  31981  bj-zfpow  31983  bj-dtru  31985  bj-sbieOLD  32020  bj-sbidmOLD  32021  bj-n0i  32127  bj-snsetex  32144  bj-tagss  32161  bj-2upln0  32204  bj-2upln1upl  32205  bj-nuliota  32210  bj-elid  32262  bj-pinftyccb  32285  bj-minftyccb  32289  bj-pinftynminfty  32291  f1omptsnlem  32359  mptsnunlem  32361  topdifinffinlem  32371  relowlpssretop  32388  1oequni2o  32392  imadifss  32554  tan2h  32571  poimirlem3  32582  poimirlem9  32588  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem22  32601  poimirlem30  32609  mblfinlem1  32616  mblfinlem2  32617  ovoliunnfl  32621  voliunnfl  32623  itg2addnclem  32631  itg2addnclem2  32632  asindmre  32665  areacirclem1  32670  fdc  32711  cntotbnd  32765  heiborlem6  32785  rrnval  32796  reheibor  32808  rngosn3  32893  prter2  33184  renegclALT  33267  mapdunirnN  35957  rntrclfvOAI  36272  diophrw  36340  rabren3dioph  36397  pellexlem6  36416  pellex  36417  frmx  36496  frmy  36497  jm2.23  36581  jm2.27dlem3  36596  axac10  36618  pw2f1ocnv  36622  kelac2lem  36652  lmhmlnmsplit  36675  pwfi2f1o  36684  frlmpwfi  36686  ifpbiidcor  36838  cnvnonrel  36913  rnnonrel  36916  resnonrel  36917  cononrel1  36919  cononrel2  36920  fvnonrel  36922  cnvcnvintabd  36925  cnvintabd  36928  rclexi  36941  rtrclex  36943  clcnvlem  36949  cnvrcl0  36951  dmtrcl  36953  rntrcl  36954  dfrtrcl5  36955  iunrelexp0  37013  dmtrclfvRP  37041  rntrclfv  37043  corcltrcl  37050  cotrclrcl  37053  0heALT  37097  frege54cor1a  37178  dssmapnvod  37334  uneqsn  37341  clsk3nimkb  37358  gneispace  37452  int-rightdistd  37505  int-sqdefd  37506  int-sqgeq0d  37511  seff  37530  expgrowthi  37554  expgrowth  37556  binomcxplemnotnn0  37577  ee233  37746  ax6e2nd  37795  in1  37808  dfvd2ani  37820  dfvd2i  37822  dfvd3i  37829  dfvd3ani  37832  e0bi  38024  uun2221  38061  uun2221p1  38062  uun2221p2  38063  en3lpVD  38102  relopabVD  38159  ax6e2ndVD  38166  ax6e2ndALT  38188  pssnssi  38312  nnf1oxpnn  38379  icof  38406  negpilt0  38433  xrgtso  38502  ioontr  38583  iccdifioo  38588  iccdifprioo  38589  fsummulc1f  38635  fsumiunss  38642  fnlimfvre2  38744  icccncfext  38773  dvcosre  38799  dvsinax  38801  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvmptmulf  38827  dvnmul  38833  dvmptfprodlem  38834  dvnprodlem2  38837  stoweidlem1  38894  stoweidlem26  38919  stoweidlem34  38927  stoweidlem44  38937  stoweid  38956  stirlinglem5  38971  dirkercncflem1  38996  fourierdlem44  39044  fourierdlem56  39055  fourierdlem62  39061  fourierdlem89  39088  fourierdlem91  39090  fourierdlem100  39099  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem108  39107  fourierdlem112  39111  fourierdlem114  39113  fouriersw  39124  rrndistlt  39186  gsumge0cl  39264  sge0tsms  39273  sge0ltfirpmpt2  39319  ovn0  39456  hoidmv1le  39484  hoidmvle  39490  ovnsubadd2lem  39535  ovolval4lem1  39539  vonioolem2  39572  smflimlem3  39659  nsssmfmbf  39665  axorbtnotaiffb  39719  axorbciffatcxorb  39721  abnotbtaxb  39731  fmtnoinf  39986  1nevenALTV  40140  nnsum3primes4  40204  tgblthelfgott  40229  tgoldbachlt  40230  tgblthelfgottOLD  40236  tgoldbachltOLD  40237  resisresindm  40320  residfi  40340  lfuhgr1v0e  40480  vdegp1bi-av  40753  pthdlem2  40974  0ewlk  41282  0pth-av  41293  konigsbergiedgw  41416  konigsbergiedgwOLD  41417  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424  konigsberglem4  41425  konigsberglem5  41426  frgrwopreg2  41488  ldepslinc  42092  alimp-no-surprise  42336  aacllem  42356  amgmwlem  42357  amgmlemALT  42358
  Copyright terms: Public domain W3C validator