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

Theorem mpbi 233
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 219 . 2 (𝜑𝜓)
41, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wb 209
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 210
This theorem is referenced by:  pm5.74i  274  notbii  323  biluk  390  pm5.19  391  pm3.24  406  dfbi  479  pm4.71i  563  pm5.32i  578  biadani  819  biadanii  821  imori  851  ori  858  pm5.16  1011  dn1  1053  3ori  1421  cadan  1611  nic-dfim  1671  nic-dfneg  1672  nic-mp  1673  nic-mpALT  1674  tbw-negdf  1701  rb-imdf  1752  nfri  1791  mpgbi  1800  19.35i  1879  nfim1  2200  19.36i  2234  sbievOLD  2332  ax6  2403  sbie  2544  sbieALT  2613  datisi  2766  disamis  2767  dimatis  2774  fresison  2775  bamalip  2778  axi12  2792  eqcomi  2831  eqtri  2845  eleqtri  2912  nfnfc  2991  neii  3013  necomi  3065  neeqtri  3083  neli  3117  nrex  3255  rexlimiv  3266  rexlimi  3301  issetiOLD  3484  vtocl2OLD  3537  eueqi  3675  euxfr2w  3686  euxfr2  3688  reuxfrd  3714  cdeqri  3732  sseqtri  3978  3sstr3i  3984  pssn2lp  4053  equncomi  4106  unssi  4136  ssini  4182  unabs  4205  inabs  4206  dfin4  4218  difid  4302  ab0orv  4307  disjdif  4393  difin0  4394  pwundif  4537  snid  4575  rabrsn  4634  iinrab2  4967  symdifv  4983  rintn0  5006  breqtri  5067  axsepgfromrep  5177  bm1.3ii  5182  ax6vsep  5183  notzfaus  5239  notzfausOLD  5240  zfpow  5244  dtru  5248  dtruALT  5266  reusv2lem4  5279  dtruALT2  5313  op1stb  5340  copsexgw  5358  copsexg  5359  uniop  5382  pwundifOLD  5434  rn0  5773  dmresi  5899  somincom  5972  cnvcnv  6027  elid  6034  rescnvcnv  6039  cnvcnvres  6040  cocnvcnv2  6089  cores2  6090  co01  6092  cnviin  6115  onunisuci  6282  iota4an  6316  fnopab  6466  mpt0  6470  fnmpti  6471  f1cnvcnv  6566  f1ovi  6635  eliman0  6687  fvco4i  6744  fmpti  6858  funiunfv  6990  oprabss  7244  relmptopab  7380  zfun  7447  tfinds2  7563  omon  7576  2nd0  7682  f1stres  7699  f2ndres  7700  cnvoprab  7744  relmpoopab  7776  df1st2  7780  df2nd2  7781  fsplit  7799  fsplitOLD  7800  reldmtpos  7887  dftpos4  7898  tpostpos  7899  tpos0  7909  wfrlem4  7945  smo0  7982  tfrlem14  8014  tfrlem16  8016  rdgsucg  8046  rdglimg  8048  frfnom  8057  oawordeulem  8167  uniixp  8472  dfdom2  8522  ssdomg  8542  xpcomf1o  8593  sbthlem5  8619  limensuci  8681  fiint  8783  fidomdm  8789  residfi  8793  pwfilem  8806  mptfi  8811  fisn  8879  dffi3  8883  ordtypelem6  8975  ordtypelem7  8976  wemaplem2  8999  harwdom  9043  suc11reg  9070  zfinf  9090  axinf2  9091  noinfep  9111  cantnfvalf  9116  cantnflt  9123  cantnf0  9126  cantnf  9144  tz9.1c  9160  tc2  9172  r111  9192  r1tr2  9194  r1ordg  9195  r1sssuc  9200  r1val1  9203  tz9.13  9208  r1elssi  9222  pwwf  9224  rankopb  9269  rankeq0b  9277  ranksuc  9282  rankmapu  9295  rankxplim3  9298  rankxpsuc  9299  cp  9308  karden  9312  card0  9375  cardlim  9389  cardom  9403  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  11611  nnne0  11659  halflt1  11843  nn0ssz  11991  3halfnz  12049  zeo  12056  numlt  12111  numltc  12112  le9lt10  12113  decle  12120  uzf  12234  xaddf  12605  xsubge0  12642  xmulf  12653  ixxf  12736  ixxssxr  12738  iooval2  12759  ioof  12825  unirnioo  12827  dfioo2  12828  fzval2  12888  fzf  12889  0nelfz1  12921  fz10  12923  fzpreddisj  12951  4fvwrd4  13022  fzof  13030  fzo0  13056  fldiv4p1lem1div2  13200  fldiv4lem1div2  13202  om2uzoi  13318  faclbnd4lem1  13649  hashkf  13688  hashgval  13689  hashinf  13691  hashresfn  13696  hashnn0n0nn  13748  hashge3el3dif  13840  rev0  14117  s2dm  14243  f1oun2prg  14270  trclublem  14346  sqrt2gt1lt2  14625  limsupgord  14820  fclim  14901  fsumrelem  15153  ackbijnn  15174  incexclem  15182  incexc  15183  arisum2  15207  georeclim  15219  geoisumr  15225  0.999...  15228  risefall0lem  15371  ege2le3  15434  sin0  15493  ef01bndlem  15528  cos2bnd  15532  cos01gt0  15535  sincos2sgn  15538  sin4lt0  15539  rpnnen2lem3  15560  rpnnen2lem9  15566  rexpen  15572  cnso  15591  dvdslelem  15650  divalglem1  15734  divalglem5  15737  divalglem6  15738  divalglem10  15742  flodddiv4  15753  0bits  15777  sadcf  15791  sadcadd  15796  bitsshft  15813  smupf  15816  gcdf  15850  eucalgf  15916  2prm  16025  dfphi2  16100  pockthi  16232  prmrec  16247  vdwapf  16297  vdwlem6  16311  karatsuba  16409  1259lem5  16459  2503lem3  16463  4001lem4  16468  structcnvcnv  16488  structfn  16491  strleun  16582  prdsval  16719  prdsds  16728  imasvscafn  16801  xpsff1o  16831  wunnat  17217  eldmcoa  17316  coapm  17322  catcfuccl  17360  catcxpccl  17448  yonedainv  17522  smndex1bas  18062  smndex1n0mnd  18068  grpinvfvi  18137  mulgfvi  18221  symgsssg  18586  symgfisg  18587  psgnunilem5  18613  sylow3lem2  18744  oppglsm  18758  efgmf  18830  efgval  18834  efgsf  18846  0frgp  18896  dmdprd  19111  dprdval  19116  invrfval  19417  drngui  19499  rmodislmod  19693  lssintcl  19727  cnfldfun  20101  cnfld0  20113  cnfld1  20114  cnfldsub  20117  xrsds  20132  psgnghm  20267  zrhpsgnmhm  20271  recrng  20308  ocv1  20366  dsmmbas2  20424  mplsubrglem  20675  opsrtoslem2  20722  mdetralt  21211  maducoeval2  21243  eltpsi  21547  unitg  21570  fctop  21607  cctop  21609  ppttop  21610  epttop  21612  leordtvallem1  21813  leordtvallem2  21814  iccordt  21817  iscnp2  21842  discmp  22001  conncompcld  22037  1stcrestlem  22055  2ndcdisj  22059  topnlly  22094  disllycmp  22101  dis1stc  22102  txuni2  22168  xkotf  22188  dfac14lem  22220  prdstps  22232  txindis  22237  tx1stc  22253  xkohaus  22256  xkoptsub  22257  cnmpt1st  22271  cnmpt2nd  22272  ptcmpfi  22416  trfil1  22489  fin1aufil  22535  tgpconncompeqg  22715  tgpconncomp  22716  trust  22833  met1stc  23126  dscmet  23177  retopon  23367  cnfldtopon  23386  xrsxmet  23412  xrsmopn  23415  iimulcn  23541  icopnfhmeo  23546  iccpnfhmeo  23548  xrhmeo  23549  cnheiborlem  23557  lebnumii  23569  ishtpy  23575  htpycc  23583  pco1  23618  pcohtpylem  23622  pcopt  23625  pcopt2  23626  pcoass  23627  pcorevlem  23629  rrxcph  23994  rrx0el  24000  ovoliunlem3  24106  ovolicc1  24118  ovolicc2  24124  volf  24131  ioorf  24175  dyadf  24193  dyadmbl  24202  vitalilem5  24214  vitali  24215  mbfimaopnlem  24257  mbflimsup  24268  0plef  24274  i1fima  24280  i1fima2  24281  i1fd  24283  itg1ge0  24288  itg10  24290  i1f1lem  24291  i1fadd  24297  i1fmul  24298  i1fmulc  24305  mbfi1fseqlem5  24321  itg2addlem  24360  reldv  24471  dvbsss  24503  dvef  24581  lhop1lem  24614  deg1fvi  24684  plypf1  24807  coeeulem  24819  coeeu  24820  vieta1lem2  24905  aannenlem3  24924  aalioulem3  24928  dvradcnv  25014  pserulm  25015  pserdvlem2  25021  sinhalfpilem  25054  sincos4thpi  25104  tan4thpi  25105  sincos6thpi  25106  pige3ALT  25110  resinf1o  25126  tanord1  25127  tanregt0  25129  efabl  25140  relogrn  25151  dfrelog  25155  logneg  25177  logltb  25189  logcn  25236  logf1o2  25239  dvlog  25240  efopnlem2  25246  efopn  25247  logccv  25252  dvsqrt  25329  dvcnsqrt  25331  cxpcn3  25335  logblog  25376  angpined  25414  1cubr  25426  asinsin  25476  asin1  25478  reasinsin  25480  atan0  25492  atanbnd  25510  atan1  25512  log2cnv  25528  log2ub  25533  log2le1  25534  birthday  25538  amgmlem  25573  emcllem5  25583  emgt0  25590  harmonicbnd3  25591  ftalem3  25658  basellem4  25667  sgmf  25728  ppi1  25747  cht1  25748  vma1  25749  ppiltx  25760  sqff1o  25765  ppiublem1  25784  ppiublem2  25785  ppiub  25786  chtub  25794  dchreq  25840  bposlem7  25872  bposlem8  25873  bposlem9  25874  lgsdir2lem2  25908  lgsdir2lem3  25909  chebbnd1  26054  chto1ub  26058  chpo1ubb  26063  pntibndlem1  26171  tgldimor  26294  tglnfn  26339  axlowdimlem4  26737  axlowdimlem16  26749  axlowdim  26753  upgrfi  26882  lfgrnloop  26916  lfuhgr1v0e  27042  usgrexmplef  27047  usgrres  27096  vdegp1bi  27325  vtxdginducedm1lem2  27328  pthdlem2  27555  wpthswwlks2on  27745  0ewlk  27897  0pth  27908  konigsbergiedgw  28031  konigsberglem1  28035  konigsberglem2  28036  konigsberglem3  28037  konigsberglem4  28038  konigsberglem5  28039  ex-dif  28206  ex-un  28207  ex-in  28208  ex-fl  28230  avril1  28246  9p10ne21fool  28254  n0lplig  28264  cnidOLD  28363  cnnvm  28463  ipasslem8  28618  ipasslem10  28620  hvsubf  28796  normlem1  28891  normlem6  28896  normlem7  28897  norm-ii-i  28918  norm3adifii  28929  hilid  28942  hlimf  29018  hhssabloi  29043  hhssnv  29045  hhshsslem1  29048  shincli  29143  shsval2i  29168  shs0i  29230  chj0i  29236  chm1i  29237  chincli  29241  chdmm1i  29258  shjshsi  29273  chsup0  29329  h1de2bi  29335  spansnpji  29359  cmcmlem  29372  cmcmii  29378  cmcm2ii  29379  cmcm3ii  29380  pjidmi  29454  pjssmii  29462  pj0i  29474  pjocini  29479  mayetes3i  29510  df0op2  29533  hoaddcomi  29553  hoaddassi  29557  hocadddiri  29560  hocsubdiri  29561  hoaddid1i  29567  ho0coi  29569  hoid1i  29570  hoid1ri  29571  hodseqi  29575  honegsubi  29577  adj1o  29675  hoddii  29770  lnopunilem1  29791  lnopunilem2  29792  nmcopexi  29808  nmcopex  29810  nmcoplb  29811  nmcfnexi  29832  nmcfnex  29834  nmcfnlb  29835  adjbd1o  29866  adjcoi  29881  nmopcoadji  29882  opsqrlem6  29926  pjsdii  29936  pjddii  29937  pjidmcoi  29958  pjtoi  29960  pjin1i  29973  pjclem1  29976  stji1i  30023  reuxfrdf  30260  inindif  30285  iuninc  30319  fnresin  30379  rinvf1o  30383  suppss2f  30392  xppreima  30402  ofoprabco  30417  gtiso  30444  df1stres  30447  df2ndres  30448  snct  30459  padct  30465  fsuppcurry1  30471  fsuppcurry2  30472  ffsrn  30475  fpwrelmapffs  30480  fzodif1  30526  nnindf  30545  nn0min  30546  dp2lt  30571  dp2ltsuc  30572  dp2ltc  30573  dplti  30591  dpmul  30599  dpmul4  30600  ressplusf  30647  xrsclat  30698  xrge0base  30703  xrge00  30704  xrnarchi  30844  xrge0slmod  30949  ccfldsrarelvec  31113  ccfldextdgrr  31114  locfinreflem  31162  locfinref  31163  unicls  31220  sqsscirc1  31225  mhmhmeotmd  31244  rmulccn  31245  raddcn  31246  xrge0iifiso  31252  xrge0iifhmeo  31253  lmxrge0  31269  cnzh  31285  rezh  31286  qqh0  31299  qqh1  31300  qqhre  31335  rrhre  31336  esumnul  31381  esum0  31382  esumsnf  31397  esumpfinvallem  31407  esumpfinvalf  31409  esumpcvgval  31411  esumcvgsum  31421  esumsup  31422  esumcvgre  31424  sigaclfu2  31454  dmsigagen  31477  ddemeas  31569  mbfmvolf  31598  br2base  31601  omssubadd  31632  sibfof  31672  sitg0  31678  eulerpartlemt  31703  eulerpartgbij  31704  0rrv  31783  coinfliplem  31810  coinflipprob  31811  coinfliprv  31814  ballotlem2  31820  ballotlem4  31830  ballotlem5  31831  ballotlemi1  31834  ballotlem7  31867  ballotth  31869  signsplypnf  31894  signsply0  31895  signsw0g  31900  signswch  31905  signsvf0  31924  hashreprin  31965  reprfz1  31969  chtvalz  31974  hgt750lemd  31993  hgt750lem  31996  hgt750lem2  31997  bnj521  32081  bnj1098  32129  bnj1109  32132  bnj1131  32133  bnj1533  32198  bnj151  32223  bnj580  32259  bnj852  32267  bnj864  32268  bnj865  32269  bnj978  32295  bnj1021  32312  bnj907  32313  bnj1093  32326  bnj1145  32339  bnj1172  32347  bnj1174  32349  bnj1176  32351  bnj1186  32353  subfacf  32496  subfacp1lem1  32500  subfacp1lem5  32505  subfacp1lem6  32506  subfacval3  32510  erdszelem2  32513  kur14lem4  32530  ioosconn  32568  iccllysconn  32571  satfn  32676  fmlaomn0  32711  gonan0  32713  goaln0  32714  elnanelprv  32750  msrfo  32867  mthmpps  32903  problem5  32986  quad3  32987  circum  32991  axextprim  33001  axrepprim  33002  axunprim  33003  axinfprim  33006  axacprim  33007  logi  33040  bcneg1  33042  setinds  33097  dfon2lem2  33103  dfon2lem4  33105  axextdfeq  33116  poseq  33169  frrlem4  33200  nosgnn0  33239  sltsolem1  33254  bdayfo  33256  nolt02o  33273  noetalem3  33293  fobigcup  33435  snelsingles  33457  fullfunfnv  33481  fullfunfv  33482  rankaltopb  33514  rank0  33705  rankeq1o  33706  hfuni  33719  fneer  33775  neibastop1  33781  nabi1i  33816  nabi2i  33817  limsucncmpi  33867  knoppcnlem8  33913  knoppcnlem11  33916  cnndvlem1  33950  bj-consensusALT  33986  bj-dtru  34215  bj-sbidmOLD  34250  bj-n0i  34347  bj-snsetex  34360  bj-tagss  34377  bj-2upln0  34420  bj-2upln1upl  34421  bj-nuliota  34435  bj-0int  34477  bj-elid5  34545  bj-inftyexpitaufo  34578  bj-pinftyccb  34597  bj-minftyccb  34601  bj-pinftynminfty  34603  iccioo01  34702  f1omptsnlem  34714  mptsnunlem  34716  topdifinffinlem  34725  relowlpssretop  34742  1oequni2o  34746  pibt2  34795  imadifss  34990  tan2h  35007  poimirlem3  35018  poimirlem9  35024  poimirlem16  35031  poimirlem17  35032  poimirlem18  35033  poimirlem19  35034  poimirlem20  35035  poimirlem22  35037  poimirlem30  35045  mblfinlem1  35052  mblfinlem2  35053  ovoliunnfl  35057  voliunnfl  35059  itg2addnclem  35066  itg2addnclem2  35067  asindmre  35098  areacirclem1  35103  fdc  35141  cntotbnd  35192  heiborlem6  35212  rrnval  35223  reheibor  35235  rngosn3  35320  ineqcomi  35623  brcnvrabga  35717  cnvresrn  35723  moantr  35734  inxp2  35737  dfxrn2  35746  cnvcosseq  35800  refrelcosslem  35820  1cosscnvxrn  35833  redundss3  35981  refrelsredund3  35987  refrelredund3  35990  prter2  36135  renegclALT  36217  mapdunirnN  38904  lcmeprodgcdi  39256  3factsumint2  39271  3factsumint3  39272  3factsumint4  39273  3factsumint  39274  lcmineqlem4  39281  3lexlogpow5ineq1  39302  2ap1caineq  39308  metakunt6  39314  metakunt24  39332  sn-dtru  39352  sqdeccom12  39427  resubf  39463  sn-0ne2  39488  sn-subf  39508  sn-0lt1  39521  reneg1lt0  39523  dffltz  39545  rntrclfvOAI  39562  diophrw  39630  rabren3dioph  39686  pellexlem6  39705  pellex  39706  frmx  39784  frmy  39785  jm2.23  39867  jm2.27dlem3  39882  axac10  39904  pw2f1ocnv  39908  kelac2lem  39938  lmhmlnmsplit  39961  pwfi2f1o  39970  frlmpwfi  39972  ifpbiidcor  40112  alephiso2  40187  alephiso3  40188  cnvnonrel  40218  rnnonrel  40221  resnonrel  40222  cononrel1  40224  cononrel2  40225  fvnonrel  40227  cnvcnvintabd  40230  cnvintabd  40233  rclexi  40245  rtrclex  40247  clcnvlem  40253  cnvrcl0  40255  dmtrcl  40257  rntrcl  40258  dfrtrcl5  40259  iunrelexp0  40333  dmtrclfvRP  40361  rntrclfv  40363  corcltrcl  40370  cotrclrcl  40373  0heALT  40415  frege54cor1a  40496  uneqsn  40659  clsk3nimkb  40676  int-sqdefd  40820  int-sqgeq0d  40825  rr-groth  40941  rr-grothprim  40942  seff  40947  expgrowthi  40971  expgrowth  40973  binomcxplemnotnn0  40994  ee233  41159  ax6e2nd  41198  in1  41211  dfvd2ani  41223  dfvd2i  41225  dfvd3i  41232  dfvd3ani  41235  e0bi  41416  uun2221  41453  uun2221p1  41454  uun2221p2  41455  en3lpVD  41485  relopabVD  41541  ax6e2ndVD  41548  ax6e2ndALT  41570  pssnssi  41673  nnf1oxpnn  41761  icof  41786  negpilt0  41850  xrgtso  41916  supxrleubrnmptf  42029  xrpnf  42064  ioontr  42087  iccdifioo  42091  iccdifprioo  42092  uzinico2  42138  fsummulc1f  42151  fsumiunss  42156  fnlimfvre2  42258  limsupreuz  42318  limsupvaluz2  42319  limsup10ex  42354  icccncfext  42468  dvcosre  42493  dvsinax  42494  ioodvbdlimc1lem2  42513  ioodvbdlimc2lem  42515  dvmptmulf  42518  dvnmul  42524  dvmptfprodlem  42525  dvnprodlem2  42528  stoweidlem1  42582  stoweidlem26  42607  stoweidlem34  42615  stoweidlem44  42625  stoweid  42644  stirlinglem5  42659  dirkercncflem1  42684  fourierdlem44  42732  fourierdlem56  42743  fourierdlem62  42749  fourierdlem89  42776  fourierdlem91  42778  fourierdlem100  42787  fourierdlem102  42789  fourierdlem103  42790  fourierdlem104  42791  fourierdlem108  42795  fourierdlem112  42799  fourierdlem114  42801  fouriersw  42812  rrndistlt  42871  gsumge0cl  42949  sge0tsms  42958  sge0ltfirpmpt2  43004  ovn0  43144  hoidmv1le  43172  hoidmvle  43178  ovnsubadd2lem  43223  ovolval4lem1  43227  vonioolem2  43259  smflimlem3  43345  nsssmfmbf  43351  axorbtnotaiffb  43435  axorbciffatcxorb  43437  abnotbtaxb  43447  euabsneu  43559  sprval  43935  fmtnoinf  43992  1nevenALTV  44148  nfermltl8rev  44199  nfermltl2rev  44200  nnsum3primes4  44245  tgblthelfgott  44272  tgoldbachlt  44273  ldepslinc  44857  ackval42  45049  rrx2plordso  45077  alimp-no-surprise  45248  aacllem  45268  amgmwlem  45269  amgmlemALT  45270
  Copyright terms: Public domain W3C validator