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

Theorem mpbi 231
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 217 . 2 (𝜑𝜓)
41, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wb 207
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 208
This theorem is referenced by:  pm5.74i  272  notbii  321  biluk  387  pm5.19  388  pm3.24  403  dfbi  476  pm4.71i  560  pm5.32i  575  biadani  816  biadanii  818  imori  848  ori  855  pm5.16  1007  dn1  1049  3ori  1416  cadan  1601  nic-dfim  1661  nic-dfneg  1662  nic-mp  1663  nic-mpALT  1664  tbw-negdf  1691  rb-imdf  1742  nfri  1781  mpgbi  1790  19.35i  1870  nfim1  2190  19.36i  2224  sbievOLD  2323  ax6  2395  sbie  2540  sbieALT  2609  datisi  2763  disamis  2764  dimatis  2771  fresison  2772  bamalip  2775  axi12  2789  axi12OLD  2790  eqcomi  2830  eqtri  2844  eleqtri  2911  neii  3018  necomi  3070  neeqtri  3088  neli  3125  nrex  3269  rexlimiv  3280  rexlimi  3315  issetiOLD  3510  vtocl2OLD  3563  eueqi  3699  euxfr2w  3710  euxfr2  3712  reuxfrd  3738  cdeqri  3756  sseqtri  4002  3sstr3i  4008  pssn2lp  4077  equncomi  4130  unssi  4160  ssini  4207  unabs  4230  inabs  4231  dfin4  4243  difid  4329  ab0orv  4334  disjdif  4419  difin0  4420  snid  4593  rabrsn  4654  iinrab2  4984  symdifv  5000  rintn0  5022  breqtri  5083  axsepgfromrep  5193  bm1.3ii  5198  ax6vsep  5199  notzfaus  5254  notzfausOLD  5255  zfpow  5259  dtru  5263  dtruALT  5280  reusv2lem4  5293  dtruALT2  5327  op1stb  5355  copsexgw  5373  copsexg  5374  uniop  5397  pwunss  5447  pwundif  5450  pwundifOLD  5451  rn0  5790  dmresi  5915  somincom  5988  cnvcnv  6043  elid  6050  rescnvcnv  6055  cnvcnvres  6056  cocnvcnv2  6105  cores2  6106  co01  6108  cnviin  6131  onunisuci  6298  iota4an  6331  fnopab  6480  mpt0  6484  fnmpti  6485  f1cnvcnv  6578  f1ovi  6647  eliman0  6699  fvco4i  6756  fmpti  6869  funiunfv  6998  oprabss  7249  relmptopab  7384  zfun  7451  tfinds2  7566  omon  7579  2nd0  7687  f1stres  7704  f2ndres  7705  cnvoprab  7749  relmpoopab  7780  df1st2  7784  df2nd2  7785  fsplit  7803  fsplitOLD  7804  reldmtpos  7891  dftpos4  7902  tpostpos  7903  tpos0  7913  wfrlem4  7949  smo0  7986  tfrlem14  8018  tfrlem16  8020  rdgsucg  8050  rdglimg  8052  frfnom  8061  oawordeulem  8170  uniixp  8474  dfdom2  8524  ssdomg  8544  xpcomf1o  8595  sbthlem5  8620  pwdom  8658  limensuci  8682  fiint  8784  fidomdm  8790  residfi  8794  pwfilem  8807  mptfi  8812  fisn  8880  dffi3  8884  ordtypelem6  8976  ordtypelem7  8977  wemaplem2  9000  wdompwdom  9031  harwdom  9043  suc11reg  9071  zfinf  9091  axinf2  9092  noinfep  9112  cantnfvalf  9117  cantnflt  9124  cantnf0  9127  cantnf  9145  tz9.1c  9161  tc2  9173  r111  9193  r1tr2  9195  r1ordg  9196  r1sssuc  9201  r1val1  9204  tz9.13  9209  r1elssi  9223  pwwf  9225  rankopb  9270  rankeq0b  9278  ranksuc  9283  rankmapu  9296  rankxplim  9297  rankxplim3  9299  rankxpsuc  9300  cp  9309  karden  9313  card0  9376  cardlim  9390  cardom  9404  infxpenlem  9428  alephsuc2  9495  alephgeom  9497  unialeph  9516  dfac4  9537  dfacacn  9556  dju1dif  9587  dju1p1e2  9588  infdju1  9604  ackbij1lem13  9643  ackbij2  9654  cf0  9662  cfsuc  9668  cfom  9675  cfslb2n  9679  ominf4  9723  fin23lem17  9749  fin23lem28  9751  fin23lem30  9753  fin23lem31  9754  fin23lem40  9762  isfin1-3  9797  dfacfin7  9810  fin1a2lem6  9816  itunitc1  9831  axcc3  9849  dcomex  9858  axdc2lem  9859  axcclem  9868  zfac  9871  ac3  9873  ackm  9876  axac2  9877  axac  9878  axaci  9879  cardeqv  9880  numth2  9882  numth  9883  dmct  9935  brdom3  9939  fin71ac  9944  cardf  9961  aleph1  9982  cfpwsdom  9995  smobeth  9997  zfcndrep  10025  zfcndpow  10027  zfcndac  10030  gch2  10086  wunex3  10152  tskpr  10181  inar1  10186  rankcf  10188  tskcard  10192  tskuni  10194  grothpw  10237  axgroth4  10243  grothprim  10245  inaprc  10247  dmaddpi  10301  dmmulpi  10302  1lt2pi  10316  addpqf  10355  mulpqf  10357  1lt2nq  10384  supsrlem  10522  ssxr  10699  gtso  10711  subf  10877  negne0i  10950  mulnzcnopr  11275  infrenegsup  11613  nnne0  11660  halflt1  11844  nn0ssz  11992  3halfnz  12050  zeo  12057  numlt  12112  numltc  12113  le9lt10  12114  decle  12121  uzf  12235  xaddf  12607  xsubge0  12644  xmulf  12655  ixxf  12738  ixxssxr  12740  iooval2  12761  ioof  12825  unirnioo  12827  dfioo2  12828  fzval2  12885  fzf  12886  0nelfz1  12916  fz10  12918  fzpreddisj  12946  4fvwrd4  13017  fzof  13025  fzo0  13051  fldiv4p1lem1div2  13195  fldiv4lem1div2  13197  om2uzoi  13313  faclbnd4lem1  13643  hashkf  13682  hashgval  13683  hashinf  13685  hashresfn  13690  hashnn0n0nn  13742  hashbclem  13800  hashge3el3dif  13834  wrdexgOLD  13862  rev0  14116  s2dm  14242  f1oun2prg  14269  trclublem  14345  sqrt2gt1lt2  14624  limsupgord  14819  fclim  14900  fsumrelem  15152  ackbijnn  15173  incexclem  15181  incexc  15182  arisum2  15206  georeclim  15218  geoisumr  15224  0.999...  15227  risefall0lem  15370  ege2le3  15433  sin0  15492  ef01bndlem  15527  cos2bnd  15531  cos01gt0  15534  sincos2sgn  15537  sin4lt0  15538  rpnnen2lem3  15559  rpnnen2lem9  15565  rexpen  15571  cnso  15590  dvdslelem  15649  n2dvds1OLD  15708  divalglem1  15735  divalglem5  15738  divalglem6  15739  divalglem10  15743  flodddiv4  15754  0bits  15778  sadcf  15792  sadcadd  15797  bitsshft  15814  smupf  15817  gcdf  15851  eucalgf  15917  2prm  16026  dfphi2  16101  pockthi  16233  prmrec  16248  vdwapf  16298  vdwlem6  16312  karatsuba  16410  1259lem5  16458  2503lem3  16462  4001lem4  16467  structcnvcnv  16487  structfn  16490  strleun  16581  prdsval  16718  prdsds  16727  imasvscafn  16800  xpsff1o  16830  sscpwex  17075  wunfunc  17159  wunnat  17216  eldmcoa  17315  coapm  17321  catcfuccl  17359  catcxpccl  17447  yonedainv  17521  grpinvfvi  18086  mulgfvi  18170  symgsssg  18526  symgfisg  18527  psgnunilem5  18553  sylow3lem2  18684  oppglsm  18698  efgmf  18770  efgval  18774  efgsf  18786  0frgp  18836  dmdprd  19051  dprdval  19056  invrfval  19354  drngui  19439  rmodislmod  19633  lssintcl  19667  mplsubrglem  20149  opsrtoslem2  20195  cnfldfun  20487  cnfld0  20499  cnfld1  20500  cnfldsub  20503  xrsds  20518  psgnghm  20654  zrhpsgnmhm  20658  recrng  20695  ocv1  20753  dsmmbas2  20811  mdetralt  21147  maducoeval2  21179  eltpsi  21482  unitg  21505  fctop  21542  cctop  21544  ppttop  21545  epttop  21547  leordtvallem1  21748  leordtvallem2  21749  iccordt  21752  iscnp2  21777  discmp  21936  conncompcld  21972  1stcrestlem  21990  2ndcdisj  21994  topnlly  22029  disllycmp  22036  dis1stc  22037  txuni2  22103  xkotf  22123  dfac14lem  22155  prdstps  22167  txindis  22172  tx1stc  22188  xkohaus  22191  xkoptsub  22192  cnmpt1st  22206  cnmpt2nd  22207  ptcmpfi  22351  trfil1  22424  fin1aufil  22470  tgpconncompeqg  22649  tgpconncomp  22650  tsmsres  22681  trust  22767  met1stc  23060  dscmet  23111  retopon  23301  cnfldtopon  23320  xrsxmet  23346  xrsmopn  23349  iimulcn  23471  icopnfhmeo  23476  iccpnfhmeo  23478  xrhmeo  23479  cnheiborlem  23487  lebnumii  23499  ishtpy  23505  htpycc  23513  pco1  23548  pcohtpylem  23552  pcopt  23555  pcopt2  23556  pcoass  23557  pcorevlem  23559  cfilresi  23827  rrxcph  23924  rrx0el  23930  ovoliunlem3  24034  ovolicc1  24046  ovolicc2  24052  volf  24059  ioorf  24103  dyadf  24121  dyadmbl  24130  vitalilem5  24142  vitali  24143  mbfimaopnlem  24185  mbflimsup  24196  0plef  24202  i1fima  24208  i1fima2  24209  i1fd  24211  itg1ge0  24216  itg10  24218  i1f1lem  24219  i1fadd  24225  i1fmul  24226  i1fmulc  24233  mbfi1fseqlem5  24249  itg2addlem  24288  reldv  24397  dvbsss  24429  dvef  24506  lhop1lem  24539  deg1fvi  24608  plypf1  24731  coeeulem  24743  coeeu  24744  vieta1lem2  24829  aannenlem3  24848  aalioulem3  24852  dvradcnv  24938  pserulm  24939  pserdvlem2  24945  sinhalfpilem  24978  sincos4thpi  25028  tan4thpi  25029  sincos6thpi  25030  pige3ALT  25034  resinf1o  25047  tanord1  25048  tanregt0  25050  efabl  25061  relogrn  25072  dfrelog  25076  logneg  25098  logltb  25110  logcn  25157  logf1o2  25160  dvlog  25161  efopnlem2  25167  efopn  25168  logccv  25173  dvsqrt  25250  dvcnsqrt  25252  cxpcn3  25256  logblog  25297  angpined  25335  1cubr  25347  asinsin  25397  asin1  25399  reasinsin  25401  atan0  25413  atanbnd  25431  atan1  25433  log2cnv  25450  log2ub  25455  log2le1  25456  birthday  25460  amgmlem  25495  emcllem5  25505  emgt0  25512  harmonicbnd3  25513  ftalem3  25580  basellem4  25589  sgmf  25650  ppi1  25669  cht1  25670  vma1  25671  ppiltx  25682  sqff1o  25687  ppiublem1  25706  ppiublem2  25707  ppiub  25708  chtub  25716  dchreq  25762  bposlem7  25794  bposlem8  25795  bposlem9  25796  lgsdir2lem2  25830  lgsdir2lem3  25831  chebbnd1  25976  chto1ub  25980  chpo1ubb  25985  pntibndlem1  26093  tgldimor  26216  tglnfn  26261  axlowdimlem4  26659  axlowdimlem16  26671  axlowdim  26675  upgrfi  26804  lfgrnloop  26838  lfuhgr1v0e  26964  usgrexmplef  26969  usgrres  27018  vdegp1bi  27247  vtxdginducedm1lem2  27250  pthdlem2  27477  wpthswwlks2on  27668  0ewlk  27821  0pth  27832  konigsbergiedgw  27955  konigsberglem1  27959  konigsberglem2  27960  konigsberglem3  27961  konigsberglem4  27962  konigsberglem5  27963  ex-dif  28130  ex-un  28131  ex-in  28132  ex-fl  28154  avril1  28170  9p10ne21fool  28178  n0lplig  28188  cnidOLD  28287  cnnvm  28387  ipasslem8  28542  ipasslem10  28544  hvsubf  28720  normlem1  28815  normlem6  28820  normlem7  28821  norm-ii-i  28842  norm3adifii  28853  hilid  28866  hlimf  28942  hhssabloi  28967  hhssnv  28969  hhshsslem1  28972  shincli  29067  shsval2i  29092  shs0i  29154  chj0i  29160  chm1i  29161  chincli  29165  chdmm1i  29182  shjshsi  29197  chsup0  29253  h1de2bi  29259  spansnpji  29283  cmcmlem  29296  cmcmii  29302  cmcm2ii  29303  cmcm3ii  29304  pjidmi  29378  pjssmii  29386  pj0i  29398  pjocini  29403  mayetes3i  29434  df0op2  29457  hoaddcomi  29477  hoaddassi  29481  hocadddiri  29484  hocsubdiri  29485  hoaddid1i  29491  ho0coi  29493  hoid1i  29494  hoid1ri  29495  hodseqi  29499  honegsubi  29501  adj1o  29599  hoddii  29694  lnopunilem1  29715  lnopunilem2  29716  nmcopexi  29732  nmcopex  29734  nmcoplb  29735  nmcfnexi  29756  nmcfnex  29758  nmcfnlb  29759  adjbd1o  29790  adjcoi  29805  nmopcoadji  29806  opsqrlem6  29850  pjsdii  29860  pjddii  29861  pjidmcoi  29882  pjtoi  29884  pjin1i  29897  pjclem1  29900  stji1i  29947  reuxfrdf  30183  inindif  30206  iuninc  30241  fnresin  30300  rinvf1o  30304  suppss2f  30313  xppreima  30323  ofoprabco  30338  gtiso  30363  df1stres  30366  df2ndres  30367  snct  30376  padct  30382  fsuppcurry1  30388  fsuppcurry2  30389  ffsrn  30392  fpwrelmapffs  30397  fzodif1  30443  nnindf  30462  nn0min  30464  dp2lt  30489  dp2ltsuc  30490  dp2ltc  30491  dplti  30509  dpmul  30517  dpmul4  30518  ressplusf  30565  xrsclat  30595  xrge0base  30600  xrge00  30601  xrnarchi  30741  xrge0slmod  30845  ccfldsrarelvec  30956  ccfldextdgrr  30957  locfinreflem  31004  locfinref  31005  unicls  31046  sqsscirc1  31051  mhmhmeotmd  31070  rmulccn  31071  raddcn  31072  xrge0iifiso  31078  xrge0iifhmeo  31079  lmxrge0  31095  cnzh  31111  rezh  31112  qqh0  31125  qqh1  31126  qqhre  31161  rrhre  31162  esumnul  31207  esum0  31208  esumsnf  31223  esumpfinvallem  31233  esumpfinvalf  31235  esumpcvgval  31237  esumcvgsum  31247  esumsup  31248  esumcvgre  31250  sigaclfu2  31280  dmsigagen  31303  ldgenpisyslem1  31322  ddemeas  31395  imambfm  31420  mbfmvolf  31424  br2base  31427  omssubadd  31458  sibfof  31498  sitg0  31504  eulerpartlemt  31529  eulerpartgbij  31530  0rrv  31609  coinfliplem  31636  coinflipprob  31637  coinfliprv  31640  ballotlem2  31646  ballotlem4  31656  ballotlem5  31657  ballotlemi1  31660  ballotlem7  31693  ballotth  31695  signsplypnf  31720  signsply0  31721  signsw0g  31726  signswch  31731  signsvf0  31750  hashreprin  31791  reprfz1  31795  chtvalz  31800  hgt750lemd  31819  hgt750lem  31822  hgt750lem2  31823  bnj521  31907  bnj1098  31955  bnj1109  31958  bnj1131  31959  bnj1533  32024  bnj151  32049  bnj580  32085  bnj852  32093  bnj864  32094  bnj865  32095  bnj978  32121  bnj1021  32136  bnj907  32137  bnj1093  32150  bnj1145  32163  bnj1172  32171  bnj1174  32173  bnj1176  32175  bnj1186  32177  subfacf  32320  subfacp1lem1  32324  subfacp1lem5  32329  subfacp1lem6  32330  subfacval3  32334  erdszelem2  32337  kur14lem4  32354  ioosconn  32392  iccllysconn  32395  satfn  32500  fmlaomn0  32535  gonan0  32537  goaln0  32538  elnanelprv  32574  msrfo  32691  mthmpps  32727  problem5  32810  quad3  32811  circum  32815  axextprim  32825  axrepprim  32826  axunprim  32827  axinfprim  32830  axacprim  32831  logi  32864  bcneg1  32866  setinds  32921  dfon2lem2  32927  dfon2lem4  32929  axextdfeq  32940  poseq  32993  frrlem4  33024  nosgnn0  33063  sltsolem1  33078  bdayfo  33080  nolt02o  33097  noetalem3  33117  fobigcup  33259  snelsingles  33281  fullfunfnv  33305  fullfunfv  33306  rankaltopb  33338  rank0  33529  rankeq1o  33530  hfuni  33543  fneer  33599  neibastop1  33605  nabi1i  33640  nabi2i  33641  limsucncmpi  33691  knoppcnlem8  33737  knoppcnlem11  33740  cnndvlem1  33774  bj-consensusALT  33810  bj-dtru  34037  bj-sbidmOLD  34072  bj-n0i  34160  bj-snsetex  34173  bj-tagss  34190  bj-2upln0  34233  bj-2upln1upl  34234  bj-nuliota  34245  bj-0int  34288  bj-elid5  34354  bj-inftyexpitaufo  34377  bj-pinftyccb  34396  bj-minftyccb  34400  bj-pinftynminfty  34402  f1omptsnlem  34500  mptsnunlem  34502  topdifinffinlem  34511  relowlpssretop  34528  1oequni2o  34532  pibt2  34581  imadifss  34749  tan2h  34766  poimirlem3  34777  poimirlem9  34783  poimirlem16  34790  poimirlem17  34791  poimirlem18  34792  poimirlem19  34793  poimirlem20  34794  poimirlem22  34796  poimirlem30  34804  mblfinlem1  34811  mblfinlem2  34812  ovoliunnfl  34816  voliunnfl  34818  itg2addnclem  34825  itg2addnclem2  34826  asindmre  34859  areacirclem1  34864  fdc  34903  cntotbnd  34957  heiborlem6  34977  rrnval  34988  reheibor  35000  rngosn3  35085  ineqcomi  35388  brcnvrabga  35482  cnvresrn  35488  moantr  35499  inxp2  35501  dfxrn2  35510  cnvcosseq  35564  refrelcosslem  35584  1cosscnvxrn  35597  redundss3  35745  refrelsredund3  35751  refrelredund3  35754  prter2  35899  renegclALT  35981  mapdunirnN  38668  sn-dtru  38991  sqdeccom12  39055  resubf  39091  sn-0ne2  39116  sn-0lt1  39126  dffltz  39151  rntrclfvOAI  39168  diophrw  39236  rabren3dioph  39292  pellexlem6  39311  pellex  39312  frmx  39390  frmy  39391  jm2.23  39473  jm2.27dlem3  39488  axac10  39510  pw2f1ocnv  39514  kelac2lem  39544  lmhmlnmsplit  39567  pwfi2f1o  39576  frlmpwfi  39578  ifpbiidcor  39720  alephiso2  39797  alephiso3  39798  cnvnonrel  39828  rnnonrel  39831  resnonrel  39832  cononrel1  39834  cononrel2  39835  fvnonrel  39837  cnvcnvintabd  39840  cnvintabd  39843  rclexi  39855  rtrclex  39857  clcnvlem  39863  cnvrcl0  39865  dmtrcl  39867  rntrcl  39868  dfrtrcl5  39869  iunrelexp0  39927  dmtrclfvRP  39955  rntrclfv  39957  corcltrcl  39964  cotrclrcl  39967  0heALT  40009  frege54cor1a  40090  dssmapnvod  40246  uneqsn  40253  clsk3nimkb  40270  gneispace  40364  int-sqdefd  40415  int-sqgeq0d  40420  rr-groth  40515  rr-grothprim  40516  seff  40521  expgrowthi  40545  expgrowth  40547  binomcxplemnotnn0  40568  ee233  40733  ax6e2nd  40772  in1  40785  dfvd2ani  40797  dfvd2i  40799  dfvd3i  40806  dfvd3ani  40809  e0bi  40990  uun2221  41027  uun2221p1  41028  uun2221p2  41029  en3lpVD  41059  relopabVD  41115  ax6e2ndVD  41122  ax6e2ndALT  41144  pssnssi  41248  nnf1oxpnn  41337  icof  41362  negpilt0  41426  xrgtso  41493  supxrleubrnmptf  41607  xrpnf  41642  ioontr  41667  iccdifioo  41671  iccdifprioo  41672  uzinico2  41718  fsummulc1f  41731  fsumiunss  41736  fnlimfvre2  41838  limsupreuz  41898  limsupvaluz2  41899  limsup10ex  41934  icccncfext  42050  dvcosre  42076  dvsinax  42077  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvmptmulf  42102  dvnmul  42108  dvmptfprodlem  42109  dvnprodlem2  42112  stoweidlem1  42167  stoweidlem26  42192  stoweidlem34  42200  stoweidlem44  42210  stoweid  42229  stirlinglem5  42244  dirkercncflem1  42269  fourierdlem44  42317  fourierdlem56  42328  fourierdlem62  42334  fourierdlem89  42361  fourierdlem91  42363  fourierdlem100  42372  fourierdlem102  42374  fourierdlem103  42375  fourierdlem104  42376  fourierdlem108  42380  fourierdlem112  42384  fourierdlem114  42386  fouriersw  42397  rrndistlt  42456  gsumge0cl  42534  sge0tsms  42543  sge0ltfirpmpt2  42589  ovn0  42729  hoidmv1le  42757  hoidmvle  42763  ovnsubadd2lem  42808  ovolval4lem1  42812  vonioolem2  42844  smflimlem3  42930  nsssmfmbf  42936  axorbtnotaiffb  43020  axorbciffatcxorb  43022  abnotbtaxb  43032  euabsneu  43144  sprval  43488  fmtnoinf  43545  1nevenALTV  43703  nfermltl8rev  43754  nfermltl2rev  43755  nnsum3primes4  43800  tgblthelfgott  43827  tgoldbachlt  43828  smndex1bas  43976  smndex1n0mnd  43982  ldepslinc  44462  rrx2plordso  44609  alimp-no-surprise  44780  aacllem  44800  amgmwlem  44801  amgmlemALT  44802
  Copyright terms: Public domain W3C validator