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  664  pm4.71ri  665  pm5.32i  669  pm3.24  926  pm5.16  934  biluk  974  4exmidOLD  998  dn1  1008  3ori  1387  cadan  1547  nic-dfim  1593  nic-dfneg  1594  nic-mp  1595  nic-mpALT  1596  tbw-negdf  1623  rb-imdf  1674  nfri  1714  mpgbi  1724  19.35i  1805  19.36iv  1904  19.37iv  1910  nfim1  2066  19.36i  2098  ax6  2250  sbie  2407  axi12  2599  bm1.1  2606  eqcomi  2630  eqtri  2643  eleqtri  2698  neii  2795  necomi  2847  neeqtri  2865  neli  2898  nrex  2999  rexlimi  3022  rexlimiv  3025  isseti  3207  vtocl2  3259  vtocl3  3260  eueq1  3377  euxfr2  3389  cdeqri  3419  sseqtri  3635  3sstr3i  3641  pssn2lp  3706  equncomi  3757  unssi  3786  ssini  3834  unabs  3852  inabs  3853  dfin4  3865  difid  3946  ab0orv  3951  npss0OLD  4013  disjdif  4038  difin0  4039  snid  4206  rabrsn  4257  iinrab2  4581  symdifv  4596  rintn0  4617  breqtri  4676  axsep  4778  bm1.3ii  4782  ax6vsep  4783  zfnuleu  4784  notzfaus  4838  zfpow  4842  dtru  4855  reusv2lem4  4870  reuxfr2d  4889  dtruALT  4897  dtruALT2  4909  op1stb  4938  copsexg  4954  uniop  4975  pwundif  5019  rn0  5375  dmresi  5455  issref  5507  somincom  5528  cnvcnv  5584  cnvcnvOLD  5585  rescnvcnv  5595  cnvcnvres  5596  cnvsn  5616  cocnvcnv2  5645  cores2  5646  co01  5648  cnviin  5670  onunisuci  5839  iota4an  5868  fnopab  6016  mpt0  6019  fnmpti  6020  f1cnvcnv  6107  f1ovi  6173  eliman0  6221  fvco4i  6274  fmpti  6381  fvsnun2  6446  funiunfv  6503  oprabss  6743  relmptopab  6880  zfun  6947  tfinds2  7060  omon  7073  2nd0  7172  f1stres  7187  f2ndres  7188  relmpt2opab  7256  df1st2  7260  df2nd2  7261  fsplit  7279  reldmtpos  7357  dftpos4  7368  tpostpos  7369  tpos0  7379  wfrlem4  7415  smo0  7452  tfrlem14  7484  tfrlem16  7486  rdgsucg  7516  rdglimg  7518  frfnom  7527  oawordeulem  7631  uniixp  7928  dfdom2  7978  ssdomg  7998  xpcomf1o  8046  sbthlem5  8071  pwdom  8109  limensuci  8133  fiint  8234  fidomdm  8240  residfi  8244  pwfilem  8257  mptfi  8262  fisn  8330  dffi3  8334  ordtypelem6  8425  ordtypelem7  8426  wemaplem2  8449  wdompwdom  8480  harwdom  8492  suc11reg  8513  zfinf  8533  axinf2  8534  noinfep  8554  cantnfvalf  8559  cantnflt  8566  cantnf0  8569  cantnf  8587  tz9.1c  8603  tc2  8615  r111  8635  r1tr2  8637  r1ordg  8638  r1sssuc  8643  r1val1  8646  tz9.13  8651  r1elssi  8665  pwwf  8667  rankopb  8712  rankeq0b  8720  ranksuc  8725  rankmapu  8738  rankxplim  8739  rankxplim3  8741  rankxpsuc  8742  cp  8751  karden  8755  card0  8781  cardlim  8795  cardom  8809  infxpenlem  8833  alephsuc2  8900  alephgeom  8902  unialeph  8921  dfac4  8942  dfacacn  8960  cda1dif  8995  pm110.643  8996  infcda1  9012  ackbij1lem13  9051  ackbij2  9062  cf0  9070  cfsuc  9076  cfom  9083  cfslb2n  9087  ominf4  9131  fin23lem17  9157  fin23lem28  9159  fin23lem30  9161  fin23lem31  9162  fin23lem40  9170  isfin1-3  9205  dfacfin7  9218  fin1a2lem6  9224  itunitc1  9239  axcc3  9257  dcomex  9266  axdc2lem  9267  axcclem  9276  zfac  9279  ac3  9281  ackm  9284  axac2  9285  axac  9286  axaci  9287  cardeqv  9288  numth2  9290  numth  9291  dmct  9343  brdom3  9347  fin71ac  9352  cardf  9369  aleph1  9390  cfpwsdom  9403  smobeth  9405  zfcndrep  9433  zfcndpow  9435  zfcndac  9438  gch2  9494  wunex3  9560  tskpr  9589  inar1  9594  rankcf  9596  tskcard  9600  tskuni  9602  grothpw  9645  axgroth4  9651  grothprim  9653  inaprc  9655  dmaddpi  9709  dmmulpi  9710  1lt2pi  9724  addpqf  9763  mulpqf  9765  1lt2nq  9792  supsrlem  9929  ssxr  10104  gtso  10116  subf  10280  negne0i  10353  mulnzcnopr  10670  infrenegsup  11003  halflt1  11247  nn0ssz  11395  3halfnz  11453  zeo  11460  numlt  11524  numltc  11525  le9lt10  11526  decle  11537  decleOLD  11540  declecOLD  11541  uzf  11687  zgt1rpn0n1  11868  xaddf  12052  xsubge0  12088  xmulf  12099  ixxf  12182  ixxssxr  12184  iooval2  12205  ioof  12268  unirnioo  12270  dfioo2  12271  xrge0neqmnf  12273  fzval2  12326  fzf  12327  0nelfz1  12357  fz10  12359  fzpreddisj  12387  4fvwrd4  12455  fzof  12463  fzo0  12488  fldiv4p1lem1div2  12631  fldiv4lem1div2  12633  om2uzoi  12749  faclbnd4lem1  13075  hashkf  13114  hashgval  13115  hashinf  13117  hashresfn  13123  hashnn0n0nn  13175  hashbclem  13231  hashge3el3dif  13263  wrdexg  13310  rev0  13507  f1oun2prg  13656  trclublem  13728  sqrt2gt1lt2  14009  limsupgord  14197  fclim  14278  fsumrelem  14533  ackbijnn  14554  incexclem  14562  incexc  14563  arisum2  14587  georeclim  14597  geoisumr  14603  0.999...  14606  0.999...OLD  14607  geoihalfsum  14608  risefall0lem  14751  ege2le3  14814  sin0  14873  ef01bndlem  14908  cos2bnd  14912  cos01gt0  14915  sincos2sgn  14918  sin4lt0  14919  rpnnen2lem3  14939  rpnnen2lem9  14945  rexpen  14951  cnso  14970  dvdslelem  15025  n2dvds1  15098  divalglem1  15111  divalglem5  15114  divalglem6  15115  divalglem10  15119  flodddiv4  15131  0bits  15155  sadcf  15169  sadcadd  15174  bitsshft  15191  smupf  15194  gcdf  15228  eucalgf  15290  2prm  15399  dfphi2  15473  pockthi  15605  prmrec  15620  vdwapf  15670  vdwap0  15674  vdwlem6  15684  karatsuba  15786  karatsubaOLD  15787  1259lem5  15836  2503lem3  15840  4001lem4  15845  structcnvcnv  15865  structfn  15868  strlemor1OLD  15963  strleun  15966  prdsval  16109  prdsds  16118  imasvscafn  16191  xpsc0  16214  xpsc1  16215  xpsff1o  16222  sscpwex  16469  wunfunc  16553  wunnat  16610  eldmcoa  16709  coapm  16715  catcfuccl  16753  catcxpccl  16841  yonedainv  16915  plusffval  17241  grpinvfvi  17457  mulgfvi  17539  symgsssg  17881  symgfisg  17882  psgnunilem5  17908  sylow3lem2  18037  oppglsm  18051  efgmf  18120  efgval  18124  efgsf  18136  0frgp  18186  dmdprd  18391  dprdval  18396  invrfval  18667  drngui  18747  scaffval  18875  rmodislmod  18925  lssintcl  18958  mplsubrglem  19433  opsrtoslem2  19479  cnfldfun  19752  cnfld0  19764  cnfld1  19765  cnfldsub  19768  xrsds  19783  psgnghm  19920  zrhpsgnmhm  19924  recrng  19961  ipffval  19987  ocv1  20017  dsmmbas2  20075  mdetralt  20408  maducoeval2  20440  eltpsi  20742  unitg  20765  fctop  20802  cctop  20804  ppttop  20805  epttop  20807  leordtvallem1  21008  leordtvallem2  21009  iccordt  21012  iscnp2  21037  discmp  21195  conncompcld  21231  1stcrestlem  21249  2ndcdisj  21253  topnlly  21288  disllycmp  21295  dis1stc  21296  txuni2  21362  xkotf  21382  dfac14lem  21414  prdstps  21426  txindis  21431  tx1stc  21447  xkohaus  21450  xkoptsub  21451  cnmpt1st  21465  cnmpt2nd  21466  ptcmpfi  21610  trfil1  21684  fin1aufil  21730  tgpconncompeqg  21909  tgpconncomp  21910  tsmsres  21941  trust  22027  met1stc  22320  dscmet  22371  retopon  22561  cnfldtopon  22580  xrsxmet  22606  xrsmopn  22609  iimulcn  22731  icopnfhmeo  22736  iccpnfhmeo  22738  xrhmeo  22739  cnheiborlem  22747  lebnumii  22759  ishtpy  22765  htpycc  22773  pco1  22809  pcohtpylem  22813  pcopt  22816  pcopt2  22817  pcoass  22818  pcorevlem  22820  cfilresi  23087  rrxcph  23174  ovoliunlem3  23266  ovolicc1  23278  ovolicc2  23284  volf  23291  ioorf  23335  dyadf  23353  dyadmbl  23362  vitalilem5  23375  vitali  23376  mbfimaopnlem  23416  mbflimsup  23427  0plef  23433  i1fima  23439  i1fima2  23440  i1fd  23442  itg1ge0  23447  itg10  23449  i1f1lem  23450  i1fadd  23456  i1fmul  23457  i1fmulc  23464  mbfi1fseqlem5  23480  itg2addlem  23519  reldv  23628  dvbsss  23660  dvef  23737  lhop1lem  23770  deg1fvi  23839  plypf1  23962  coeeulem  23974  coeeu  23975  vieta1lem2  24060  aannenlem3  24079  aalioulem3  24083  dvradcnv  24169  pserulm  24170  pserdvlem2  24176  abelthlem6  24184  sinhalfpilem  24209  sincos4thpi  24259  tan4thpi  24260  sincos6thpi  24261  pige3  24263  resinf1o  24276  tanord1  24277  tanregt0  24279  efabl  24290  relogrn  24302  dfrelog  24306  logneg  24328  logltb  24340  logcn  24387  logf1o2  24390  dvlog  24391  efopnlem2  24397  efopn  24398  logccv  24403  dvsqrt  24477  dvcnsqrt  24479  cxpcn3  24483  logblog  24524  angpined  24551  1cubr  24563  asinsin  24613  asin1  24615  reasinsin  24617  atan0  24629  atanbnd  24647  atan1  24649  log2cnv  24665  log2ub  24670  log2le1  24671  birthday  24675  amgmlem  24710  emcllem5  24720  emgt0  24727  harmonicbnd3  24728  ftalem3  24795  basellem4  24804  sgmf  24865  ppi1  24884  cht1  24885  vma1  24886  ppiltx  24897  sqff1o  24902  ppiublem1  24921  ppiublem2  24922  ppiub  24923  chtub  24931  dchreq  24977  bposlem7  25009  bposlem8  25010  bposlem9  25011  lgsdir2lem2  25045  lgsdir2lem3  25046  chebbnd1  25155  chto1ub  25159  chpo1ubb  25164  pntibndlem1  25272  tgldimor  25391  tglnfn  25436  axlowdimlem4  25819  axlowdimlem16  25831  axlowdim  25835  upgrfi  25980  lfgrnloop  26014  lfuhgr1v0e  26140  usgrexmplef  26145  usgrres  26194  vdegp1bi  26427  vtxdginducedm1lem2  26430  pthdlem2  26658  0ewlk  26968  0pth  26979  konigsbergiedgw  27101  konigsbergiedgwOLD  27102  konigsberglem1  27107  konigsberglem2  27108  konigsberglem3  27109  konigsberglem4  27110  konigsberglem5  27111  ex-dif  27264  ex-un  27265  ex-in  27266  ex-fl  27288  avril1  27303  n0lplig  27319  vcex  27417  cnidOLD  27421  cnnvm  27521  ipasslem8  27676  ipasslem10  27678  hvsubf  27856  normlem1  27951  normlem6  27956  normlem7  27957  norm-ii-i  27978  norm3adifii  27989  hilid  28002  hlimf  28078  hhssabloi  28103  hhssnv  28105  hhshsslem1  28108  shincli  28205  shsval2i  28230  shs0i  28292  chj0i  28298  chm1i  28299  chincli  28303  chdmm1i  28320  shjshsi  28335  chsup0  28391  h1de2bi  28397  spansnpji  28421  cmcmlem  28434  cmcmii  28440  cmcm2ii  28441  cmcm3ii  28442  pjidmi  28516  pjssmii  28524  pj0i  28536  pjocini  28541  mayetes3i  28572  df0op2  28595  hoaddcomi  28615  hoaddassi  28619  hocadddiri  28622  hocsubdiri  28623  hoaddid1i  28629  ho0coi  28631  hoid1i  28632  hoid1ri  28633  hodseqi  28637  honegsubi  28639  adj1o  28737  hoddii  28832  lnopunilem1  28853  lnopunilem2  28854  nmcopexi  28870  nmcopex  28872  nmcoplb  28873  nmcfnexi  28894  nmcfnex  28896  nmcfnlb  28897  adjbd1o  28928  adjcoi  28943  nmopcoadji  28944  opsqrlem6  28988  pjsdii  28998  pjddii  28999  pjidmcoi  29020  pjtoi  29022  pjin1i  29035  pjclem1  29038  stji1i  29085  reuxfr3d  29313  inindif  29337  iuninc  29363  fnresin  29414  rinvf1o  29416  suppss2f  29423  xppreima  29433  ofoprabco  29449  funcnvmptOLD  29452  gtiso  29463  df1stres  29466  df2ndres  29467  snct  29476  padct  29482  ffsrn  29489  fpwrelmapffs  29494  nnindf  29550  nn0min  29552  dp2lt  29577  dp2ltsuc  29578  dp2ltc  29579  dplti  29598  dpmul  29606  dpmul4  29607  ressplusf  29635  xrsclat  29665  xrge0base  29670  xrge00  29671  xrnarchi  29723  xrge0slmod  29829  locfinreflem  29892  locfinref  29893  unicls  29934  sqsscirc1  29939  mhmhmeotmd  29958  rmulccn  29959  raddcn  29960  xrge0iifiso  29966  xrge0iifhmeo  29967  lmxrge0  29983  cnzh  29999  rezh  30000  qqh0  30013  qqh1  30014  qqhre  30049  rrhre  30050  esumnul  30095  esum0  30096  esumsnf  30111  esumpfinvallem  30121  esumpfinvalf  30123  esumpcvgval  30125  esumcvgsum  30135  esumsup  30136  esumcvgre  30138  sigaclfu2  30169  dmsigagen  30192  ldgenpisyslem1  30211  ddemeas  30284  imambfm  30309  mbfmvolf  30313  br2base  30316  omssubadd  30347  sibfof  30387  sitg0  30393  eulerpartlemt  30418  eulerpartgbij  30419  0rrv  30498  coinfliplem  30525  coinflipprob  30526  coinfliprv  30529  ballotlem2  30535  ballotlem4  30545  ballotlem5  30546  ballotlemi1  30549  ballotlem7  30582  ballotth  30584  signsplypnf  30612  signsply0  30613  signsw0g  30618  signswch  30623  signsvf0  30642  hashreprin  30683  reprfz1  30687  chtvalz  30692  hgt750lemd  30711  hgt750lem  30714  hgt750lem2  30715  bnj521  30790  bnj1098  30839  bnj1109  30842  bnj1131  30843  bnj1533  30907  bnj151  30932  bnj580  30968  bnj852  30976  bnj864  30977  bnj865  30978  bnj978  31004  bnj1021  31019  bnj907  31020  bnj1093  31033  bnj1145  31046  bnj1172  31054  bnj1174  31056  bnj1176  31058  bnj1186  31060  subfacf  31142  subfacp1lem1  31146  subfacp1lem5  31151  subfacp1lem6  31152  subfacval3  31156  erdszelem2  31159  kur14lem4  31176  ioosconn  31214  iccllysconn  31217  msrfo  31428  mthmpps  31464  problem5  31548  quad3  31549  circum  31553  axextprim  31563  axrepprim  31564  axunprim  31565  axinfprim  31568  axacprim  31569  inffzOLD  31601  logi  31606  bcneg1  31608  setinds  31667  dfon2lem2  31673  dfon2lem4  31675  axextdfeq  31687  poseq  31734  frrlem4  31767  nosgnn0  31795  sltsolem1  31810  bdayfo  31812  nolt02o  31829  noetalem3  31849  dmscut  31902  fobigcup  31991  snelsingles  32013  fullfunfnv  32037  fullfunfv  32038  rankaltopb  32070  rank0  32261  rankeq1o  32262  hfuni  32275  fneer  32332  neibastop1  32338  nabi1i  32375  nabi2i  32376  limsucncmpi  32428  knoppcnlem8  32474  knoppcnlem11  32477  cnndvlem1  32512  bj-consensusALT  32547  bj-axsep  32777  bj-zfpow  32779  bj-dtru  32781  bj-sbidmOLD  32815  bj-n0i  32919  bj-snsetex  32935  bj-tagss  32952  bj-2upln0  32995  bj-2upln1upl  32996  bj-nuliota  33003  bj-0int  33039  bj-elid  33065  bj-pinftyccb  33088  bj-minftyccb  33092  bj-pinftynminfty  33094  f1omptsnlem  33163  mptsnunlem  33165  topdifinffinlem  33175  relowlpssretop  33192  1oequni2o  33196  imadifss  33364  tan2h  33381  poimirlem3  33392  poimirlem9  33398  poimirlem16  33405  poimirlem17  33406  poimirlem18  33407  poimirlem19  33408  poimirlem20  33409  poimirlem22  33411  poimirlem30  33419  mblfinlem1  33426  mblfinlem2  33427  ovoliunnfl  33431  voliunnfl  33433  itg2addnclem  33441  itg2addnclem2  33442  asindmre  33475  areacirclem1  33480  fdc  33521  cntotbnd  33575  heiborlem6  33595  rrnval  33606  reheibor  33618  rngosn3  33703  prter2  33992  renegclALT  34075  mapdunirnN  36765  rntrclfvOAI  37080  diophrw  37148  rabren3dioph  37205  pellexlem6  37224  pellex  37225  frmx  37304  frmy  37305  jm2.23  37389  jm2.27dlem3  37404  axac10  37426  pw2f1ocnv  37430  kelac2lem  37460  lmhmlnmsplit  37483  pwfi2f1o  37492  frlmpwfi  37494  ifpbiidcor  37645  cnvnonrel  37720  rnnonrel  37723  resnonrel  37724  cononrel1  37726  cononrel2  37727  fvnonrel  37729  cnvcnvintabd  37732  cnvintabd  37735  rclexi  37748  rtrclex  37750  clcnvlem  37756  cnvrcl0  37758  dmtrcl  37760  rntrcl  37761  dfrtrcl5  37762  iunrelexp0  37820  dmtrclfvRP  37848  rntrclfv  37850  corcltrcl  37857  cotrclrcl  37860  0heALT  37903  frege54cor1a  37984  dssmapnvod  38140  uneqsn  38147  clsk3nimkb  38164  gneispace  38258  int-sqdefd  38310  int-sqgeq0d  38315  seff  38334  expgrowthi  38358  expgrowth  38360  binomcxplemnotnn0  38381  ee233  38551  ax6e2nd  38600  in1  38613  dfvd2ani  38625  dfvd2i  38627  dfvd3i  38634  dfvd3ani  38637  e0bi  38829  uun2221  38866  uun2221p1  38867  uun2221p2  38868  en3lpVD  38906  relopabVD  38963  ax6e2ndVD  38970  ax6e2ndALT  38992  pssnssi  39109  nnf1oxpnn  39206  icof  39233  negpilt0  39311  xrgtso  39380  supxrleubrnmptf  39499  ioontr  39545  iccdifioo  39550  iccdifprioo  39551  uzinico2  39598  fsummulc1f  39608  fsumiunss  39613  fnlimfvre2  39715  limsupreuz  39775  limsupvaluz2  39776  limsup10ex  39805  icccncfext  39869  dvcosre  39895  dvsinax  39896  ioodvbdlimc1lem2  39916  ioodvbdlimc2lem  39918  dvmptmulf  39921  dvnmul  39927  dvmptfprodlem  39928  dvnprodlem2  39931  stoweidlem1  39987  stoweidlem26  40012  stoweidlem34  40020  stoweidlem44  40030  stoweid  40049  stirlinglem5  40064  dirkercncflem1  40089  fourierdlem44  40137  fourierdlem56  40148  fourierdlem62  40154  fourierdlem89  40181  fourierdlem91  40183  fourierdlem100  40192  fourierdlem102  40194  fourierdlem103  40195  fourierdlem104  40196  fourierdlem108  40200  fourierdlem112  40204  fourierdlem114  40206  fouriersw  40217  rrndistlt  40279  gsumge0cl  40357  sge0tsms  40366  sge0ltfirpmpt2  40412  ovn0  40549  hoidmv1le  40577  hoidmvle  40583  ovnsubadd2lem  40628  ovolval4lem1  40632  vonioolem2  40664  smflimlem3  40750  nsssmfmbf  40756  axorbtnotaiffb  40839  axorbciffatcxorb  40841  abnotbtaxb  40851  fmtnoinf  41219  1nevenALTV  41373  nnsum3primes4  41447  tgblthelfgott  41474  tgoldbachlt  41475  tgblthelfgottOLD  41480  tgoldbachltOLD  41481  sprval  41500  ldepslinc  42069  alimp-no-surprise  42298  aacllem  42318  amgmwlem  42319  amgmlemALT  42320
  Copyright terms: Public domain W3C validator