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

Theorem mpbi 218
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 204 . 2 (𝜑𝜓)
41, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wb 194
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 195
This theorem is referenced by:  pm5.74i  258  notbii  308  pm5.19  373  ori  388  imori  427  pm4.71i  661  pm4.71ri  662  pm5.32i  666  pm3.24  921  pm5.16  929  biluk  969  4exmid  976  dn1  999  3ori  1379  cadan  1538  nic-dfim  1584  nic-dfneg  1585  nic-mp  1586  nic-mpALT  1587  tbw-negdf  1614  rb-imdf  1665  nfri  1705  mpgbi  1714  19.35i  1793  19.36iv  1890  19.37iv  1896  nfim1  2052  19.36i  2083  ax6  2233  sbie  2391  axi12  2583  bm1.1  2590  eqcomi  2614  eqtri  2627  eleqtri  2681  neii  2779  necomi  2831  neeqtri  2849  neli  2880  nrex  2978  rexlimi  3001  rexlimiv  3004  isseti  3177  vtocl2  3229  vtocl3  3230  eueq1  3341  euxfr2  3353  cdeqri  3383  sseqtri  3595  3sstr3i  3601  pssn2lp  3665  equncomi  3716  unssi  3745  ssini  3793  unabs  3811  inabs  3812  dfin4  3821  difid  3897  ab0orv  3902  npss0OLD  3962  disjdif  3987  difin0  3988  snid  4150  rabrsn  4198  iinrab2  4509  symdifv  4524  rintn0  4542  breqtri  4598  axsep  4698  bm1.3ii  4702  ax6vsep  4703  zfnuleu  4704  notzfaus  4757  zfpow  4761  dtru  4774  reusv2lem4  4789  reuxfr2d  4808  dtruALT  4817  dtruALT2  4829  op1stb  4857  copsexg  4872  uniop  4889  pwundif  4931  rn0  5281  dmresi  5359  issref  5411  somincom  5432  cnvcnv  5487  rescnvcnv  5497  cnvcnvres  5498  cnvsn  5518  cocnvcnv2  5546  cores2  5547  co01  5549  cnviin  5571  onunisuci  5740  iota4an  5769  fnopab  5913  mpt0  5916  fnmpti  5917  f1cnvcnv  6003  f1ovi  6068  eliman0  6114  fvco4i  6167  fmpti  6272  fvsnun2  6328  funiunfv  6384  oprabss  6618  relmptopab  6754  zfun  6821  tfinds2  6928  omon  6941  2nd0  7039  f1stres  7054  f2ndres  7055  relmpt2opab  7119  df1st2  7123  df2nd2  7124  fsplit  7142  reldmtpos  7220  dftpos4  7231  tpostpos  7232  tpos0  7242  wfrlem4  7278  smo0  7315  tfrlem14  7347  tfrlem16  7349  rdgsucg  7379  rdglimg  7381  frfnom  7390  oawordeulem  7494  uniixp  7790  dfdom2  7840  ssdomg  7860  xpcomf1o  7907  sbthlem5  7932  pwdom  7970  limensuci  7994  fiint  8095  fidomdm  8101  pwfilem  8116  mptfi  8121  fisn  8189  dffi3  8193  ordtypelem6  8284  ordtypelem7  8285  wemaplem2  8308  wdompwdom  8339  harwdom  8351  suc11reg  8372  zfinf  8392  axinf2  8393  noinfep  8413  cantnfvalf  8418  cantnflt  8425  cantnf0  8428  cantnf  8446  tz9.1c  8462  tc2  8474  r111  8494  r1tr2  8496  r1ordg  8497  r1sssuc  8502  r1val1  8505  tz9.13  8510  r1elssi  8524  pwwf  8526  rankopb  8571  rankeq0b  8579  ranksuc  8584  rankmapu  8597  rankxplim  8598  rankxplim3  8600  rankxpsuc  8601  cp  8610  karden  8614  card0  8640  cardlim  8654  cardom  8668  infxpenlem  8692  alephsuc2  8759  alephgeom  8761  unialeph  8780  dfac4  8801  dfacacn  8819  cda1dif  8854  pm110.643  8855  infcda1  8871  ackbij1lem13  8910  ackbij2  8921  cf0  8929  cfsuc  8935  cfom  8942  cfslb2n  8946  ominf4  8990  fin23lem17  9016  fin23lem28  9018  fin23lem30  9020  fin23lem31  9021  fin23lem40  9029  isfin1-3  9064  dfacfin7  9077  fin1a2lem6  9083  itunitc1  9098  axcc3  9116  dcomex  9125  axdc2lem  9126  axcclem  9135  zfac  9138  ac3  9140  ackm  9143  axac2  9144  axac  9145  axaci  9146  cardeqv  9147  numth2  9149  numth  9150  brdom3  9204  fin71ac  9209  cardf  9224  aleph1  9245  cfpwsdom  9258  smobeth  9260  zfcndrep  9288  zfcndpow  9290  zfcndac  9293  gch2  9349  wunex3  9415  tskpr  9444  inar1  9449  rankcf  9451  tskcard  9455  tskuni  9457  grothpw  9500  axgroth4  9506  grothprim  9508  inaprc  9510  dmaddpi  9564  dmmulpi  9565  1lt2pi  9579  addpqf  9618  mulpqf  9620  1lt2nq  9647  supsrlem  9784  ssxr  9954  gtso  9966  subf  10130  negne0i  10203  mulnzcnopr  10518  infrenegsup  10849  halflt1  11093  nn0ssz  11227  3halfnz  11284  zeo  11291  numlt  11355  numltc  11356  le9lt10  11357  decle  11368  decleOLD  11371  declecOLD  11372  uzf  11518  zgt1rpn0n1  11699  xaddf  11884  xsubge0  11916  xmulf  11927  ixxf  12008  ixxssxr  12010  iooval2  12031  ioof  12094  unirnioo  12096  dfioo2  12097  xrge0neqmnf  12099  fzval2  12151  fzf  12152  0nelfz1  12182  fz10  12184  fzpreddisj  12211  4fvwrd4  12279  fzof  12287  fzo0  12312  fldiv4p1lem1div2  12449  fldiv4lem1div2  12451  om2uzoi  12567  faclbnd4lem1  12893  hashkf  12932  hashgval  12933  hashinf  12935  hashresfn  12938  hashnn0n0nn  12989  hashbclem  13041  hashge3el3dif  13068  wrdexg  13112  rev0  13306  f1oun2prg  13454  trclublem  13524  sqrt2gt1lt2  13805  limsupgord  13993  fclim  14074  fsumrelem  14322  ackbijnn  14341  incexclem  14349  incexc  14350  arisum2  14374  georeclim  14384  geoisumr  14390  0.999...  14393  0.999...OLD  14394  geoihalfsum  14395  risefall0lem  14538  ege2le3  14601  sin0  14660  ef01bndlem  14695  cos2bnd  14699  cos01gt0  14702  sincos2sgn  14705  sin4lt0  14706  rpnnen2lem3  14726  rpnnen2lem9  14732  rexpen  14738  cnso  14757  dvdslelem  14811  n2dvds1  14884  divalglem1  14897  divalglem5  14900  divalglem6  14901  divalglem10  14905  flodddiv4  14917  0bits  14941  sadcf  14955  sadcadd  14960  bitsshft  14977  smupf  14980  gcdf  15014  eucalgf  15076  2prm  15185  dfphi2  15259  pockthi  15391  prmrec  15406  vdwapf  15456  vdwap0  15460  vdwlem6  15470  karatsuba  15572  karatsubaOLD  15573  1259lem5  15622  2503lem3  15626  4001lem4  15631  structcnvcnv  15648  structfn  15650  strlemor1  15738  strleun  15741  prdsval  15880  prdsds  15889  imasvscafn  15962  xpsc0  15985  xpsc1  15986  xpsff1o  15993  sscpwex  16240  wunfunc  16324  wunnat  16381  eldmcoa  16480  coapm  16486  catcfuccl  16524  catcxpccl  16612  yonedainv  16686  plusffval  17012  grpinvfvi  17228  mulgfvi  17310  symgsssg  17652  symgfisg  17653  psgnunilem5  17679  sylow3lem2  17808  oppglsm  17822  efgmf  17891  efgval  17895  efgsf  17907  0frgp  17957  dmdprd  18162  dprdval  18167  invrfval  18438  drngui  18518  scaffval  18646  lssintcl  18727  mplsubrglem  19202  opsrtoslem2  19248  cnfld0  19531  cnfld1  19532  cnfldsub  19535  xrsds  19550  psgnghm  19686  zrhpsgnmhm  19690  recrng  19727  ipffval  19753  ocv1  19780  dsmmbas2  19838  mdetralt  20171  maducoeval2  20203  eltpsi  20499  unitg  20520  fctop  20556  cctop  20558  ppttop  20559  epttop  20561  leordtvallem1  20762  leordtvallem2  20763  iccordt  20766  iscnp2  20791  discmp  20949  concompcld  20985  1stcrestlem  21003  2ndcdisj  21007  topnlly  21042  disllycmp  21049  dis1stc  21050  txuni2  21116  xkotf  21136  dfac14lem  21168  prdstps  21180  txindis  21185  tx1stc  21201  xkohaus  21204  xkoptsub  21205  cnmpt1st  21219  cnmpt2nd  21220  ptcmpfi  21364  trfil1  21438  fin1aufil  21484  tgpconcompeqg  21663  tgpconcomp  21664  tsmsres  21695  trust  21781  met1stc  22073  dscmet  22124  retopon  22305  cnfldtopon  22324  xrsxmet  22348  xrsmopn  22351  iimulcn  22472  icopnfhmeo  22477  iccpnfhmeo  22479  xrhmeo  22480  cnheiborlem  22488  lebnumii  22500  ishtpy  22506  htpycc  22514  pco1  22550  pcohtpylem  22554  pcopt  22557  pcopt2  22558  pcoass  22559  pcorevlem  22561  cfilresi  22815  rrxcph  22901  ovoliunlem3  22992  ovolicc1  23004  ovolicc2  23010  volf  23017  ioorf  23060  dyadf  23078  dyadmbl  23087  vitalilem5  23100  vitali  23101  mbfimaopnlem  23141  mbflimsup  23152  0plef  23158  i1fima  23164  i1fima2  23165  i1fd  23167  itg1ge0  23172  itg10  23174  i1f1lem  23175  i1fadd  23181  i1fmul  23182  i1fmulc  23189  mbfi1fseqlem5  23205  itg2addlem  23244  reldv  23353  dvbsss  23385  dvef  23460  lhop1lem  23493  deg1fvi  23562  plypf1  23685  coeeulem  23697  coeeu  23698  vieta1lem2  23783  aannenlem3  23802  aalioulem3  23806  dvradcnv  23892  pserulm  23893  pserdvlem2  23899  abelthlem6  23907  sinhalfpilem  23932  sincos4thpi  23982  tan4thpi  23983  sincos6thpi  23984  pige3  23986  resinf1o  23999  tanord1  24000  tanregt0  24002  efabl  24013  relogrn  24025  dfrelog  24029  logneg  24051  logltb  24063  logcn  24106  logf1o2  24109  dvlog  24110  efopnlem2  24116  efopn  24117  logccv  24122  dvsqrt  24196  dvcnsqrt  24198  cxpcn3  24202  logblog  24243  angpined  24270  1cubr  24282  asinsin  24332  asin1  24334  reasinsin  24336  atan0  24348  atanbnd  24366  atan1  24368  log2cnv  24384  log2ub  24389  log2le1  24390  birthday  24394  amgmlem  24429  emcllem5  24439  emgt0  24446  harmonicbnd3  24447  ftalem3  24514  basellem4  24523  sgmf  24584  ppi1  24603  cht1  24604  vma1  24605  ppiltx  24616  sqff1o  24621  ppiublem1  24640  ppiublem2  24641  ppiub  24642  chtub  24650  dchreq  24696  bposlem7  24728  bposlem8  24729  bposlem9  24730  lgsdir2lem2  24764  lgsdir2lem3  24765  chebbnd1  24874  chto1ub  24878  chpo1ubb  24883  pntibndlem1  24991  tgldimor  25110  tglnfn  25156  axlowdimlem4  25539  axlowdimlem16  25551  axlowdim  25555  umgrafi  25613  usgraexmplef  25691  usgraexmplc  25695  usgrafilem1  25702  2trllemA  25842  wlkntrllem1  25851  wlkntrllem3  25853  0pth  25862  spthispth  25865  2pthon  25894  2pthon3v  25896  constr3trllem3  25942  constr3pthlem3  25947  konigsberg  26276  frgrawopreg2  26340  ex-dif  26434  ex-un  26435  ex-in  26436  ex-fl  26458  avril1  26473  vcoprnelem  26595  vcex  26597  cnidOLD  26601  cnnvm  26714  ipasslem8  26878  ipasslem10  26880  hvsubf  27058  normlem1  27153  normlem6  27158  normlem7  27159  norm-ii-i  27180  norm3adifii  27191  hilid  27204  hlimf  27280  hhssabloi  27305  hhssnv  27307  hhshsslem1  27310  shincli  27407  shsval2i  27432  shs0i  27494  chj0i  27500  chm1i  27501  chincli  27505  chdmm1i  27522  shjshsi  27537  chsup0  27593  h1de2bi  27599  spansnpji  27623  cmcmlem  27636  cmcmii  27642  cmcm2ii  27643  cmcm3ii  27644  pjidmi  27718  pjssmii  27726  pj0i  27738  pjocini  27743  mayetes3i  27774  df0op2  27797  hoaddcomi  27817  hoaddassi  27821  hocadddiri  27824  hocsubdiri  27825  hoaddid1i  27831  ho0coi  27833  hoid1i  27834  hoid1ri  27835  hodseqi  27839  honegsubi  27841  adj1o  27939  hoddii  28034  lnopunilem1  28055  lnopunilem2  28056  nmcopexi  28072  nmcopex  28074  nmcoplb  28075  nmcfnexi  28096  nmcfnex  28098  nmcfnlb  28099  adjbd1o  28130  adjcoi  28145  nmopcoadji  28146  opsqrlem6  28190  pjsdii  28200  pjddii  28201  pjidmcoi  28222  pjtoi  28224  pjin1i  28237  pjclem1  28240  stji1i  28287  reuxfr3d  28515  inindif  28540  iuninc  28563  fnresin  28614  rinvf1o  28616  suppss2f  28621  xppreima  28631  ofoprabco  28649  funcnvmptOLD  28652  gtiso  28663  df1stres  28666  df2ndres  28667  snct  28676  dmct  28679  padct  28687  ffsrn  28694  fpwrelmapffs  28699  nnindf  28754  nn0min  28756  ressplusf  28783  xrsclat  28813  xrge0base  28818  xrge00  28819  xrnarchi  28871  xrge0slmod  28977  locfinreflem  29037  locfinref  29038  unicls  29079  sqsscirc1  29084  mhmhmeotmd  29103  rmulccn  29104  raddcn  29105  xrge0iifiso  29111  xrge0iifhmeo  29112  lmxrge0  29128  cnzh  29144  rezh  29145  qqh0  29158  qqh1  29159  qqhre  29194  rrhre  29195  esumnul  29239  esum0  29240  esumsnf  29255  esumpfinvallem  29265  esumpfinvalf  29267  esumpcvgval  29269  esumcvgsum  29279  esumsup  29280  esumcvgre  29282  sigaclfu2  29313  dmsigagen  29336  ldgenpisyslem1  29355  ddemeas  29428  imambfm  29453  mbfmvolf  29457  br2base  29460  omssubadd  29491  sibfof  29531  sitg0  29537  eulerpartlemt  29562  eulerpartgbij  29563  0rrv  29642  coinfliplem  29669  coinflipprob  29670  coinfliprv  29673  ballotlem2  29679  ballotlem4  29689  ballotlem5  29690  ballotlemi1  29693  ballotlem7  29726  ballotth  29728  signsplypnf  29755  signsply0  29756  signsw0g  29761  signswch  29766  signsvf0  29785  bnj521  29861  bnj1098  29910  bnj1109  29913  bnj1131  29914  bnj1533  29978  bnj151  30003  bnj580  30039  bnj852  30047  bnj864  30048  bnj865  30049  bnj978  30075  bnj1021  30090  bnj907  30091  bnj1093  30104  bnj1145  30117  bnj1172  30125  bnj1174  30127  bnj1176  30129  bnj1186  30131  subfacf  30213  subfacp1lem1  30217  subfacp1lem5  30222  subfacp1lem6  30223  subfacval3  30227  erdszelem2  30230  kur14lem4  30247  iooscon  30285  iccllyscon  30288  msrfo  30499  mthmpps  30535  problem5  30619  quad3  30620  circum  30624  axextprim  30634  axrepprim  30635  axunprim  30636  axinfprim  30639  axacprim  30640  inffzOLD  30670  logi  30675  bcneg1  30677  setinds  30729  dfon2lem2  30735  dfon2lem4  30737  axextdfeq  30749  poseq  30796  frrlem4  30829  nosgnn0  30857  sltsolem1  30869  bdayfo  30876  fobigcup  30979  snelsingles  31001  fullfunfnv  31025  fullfunfv  31026  rankaltopb  31058  rank0  31249  rankeq1o  31250  hfuni  31263  fneer  31320  neibastop1  31326  nabi1i  31363  nabi2i  31364  limsucncmpi  31416  knoppcnlem8  31462  knoppcnlem11  31465  cnndvlem1  31500  bj-consensusALT  31535  bj-nfxfr  31596  bj-axsep  31790  bj-zfpow  31792  bj-dtru  31794  bj-sbieOLD  31829  bj-sbidmOLD  31830  bj-n0i  31926  bj-snsetex  31943  bj-tagss  31960  bj-2upln0  32003  bj-2upln1upl  32004  bj-nuliota  32009  bj-elid  32061  bj-pinftyccb  32084  bj-minftyccb  32088  bj-pinftynminfty  32090  f1omptsnlem  32158  mptsnunlem  32160  topdifinffinlem  32170  relowlpssretop  32187  1oequni2o  32191  imadifss  32353  tan2h  32370  poimirlem3  32381  poimirlem9  32387  poimirlem16  32394  poimirlem17  32395  poimirlem18  32396  poimirlem19  32397  poimirlem20  32398  poimirlem22  32400  poimirlem30  32408  mblfinlem1  32415  mblfinlem2  32416  ovoliunnfl  32420  voliunnfl  32422  itg2addnclem  32430  itg2addnclem2  32431  asindmre  32464  areacirclem1  32469  fdc  32510  cntotbnd  32564  heiborlem6  32584  rrnval  32595  reheibor  32607  rngosn3  32692  prter2  32983  renegclALT  33066  mapdunirnN  35756  rntrclfvOAI  36071  diophrw  36139  rabren3dioph  36196  pellexlem6  36215  pellex  36216  frmx  36295  frmy  36296  jm2.23  36380  jm2.27dlem3  36395  axac10  36417  pw2f1ocnv  36421  kelac2lem  36451  lmhmlnmsplit  36474  pwfi2f1o  36483  frlmpwfi  36485  ifpbiidcor  36637  cnvnonrel  36712  rnnonrel  36715  resnonrel  36716  cononrel1  36718  cononrel2  36719  fvnonrel  36721  cnvcnvintabd  36724  cnvintabd  36727  rclexi  36740  rtrclex  36742  clcnvlem  36748  cnvrcl0  36750  dmtrcl  36752  rntrcl  36753  dfrtrcl5  36754  iunrelexp0  36812  dmtrclfvRP  36840  rntrclfv  36842  corcltrcl  36849  cotrclrcl  36852  0heALT  36896  frege54cor1a  36977  dssmapnvod  37133  uneqsn  37140  clsk3nimkb  37157  gneispace  37251  int-rightdistd  37304  int-sqdefd  37305  int-sqgeq0d  37310  seff  37329  expgrowthi  37353  expgrowth  37355  binomcxplemnotnn0  37376  ee233  37545  ax6e2nd  37594  in1  37607  dfvd2ani  37619  dfvd2i  37621  dfvd3i  37628  dfvd3ani  37631  e0bi  37823  uun2221  37860  uun2221p1  37861  uun2221p2  37862  en3lpVD  37901  relopabVD  37958  ax6e2ndVD  37965  ax6e2ndALT  37987  pssnssi  38111  nnf1oxpnn  38178  icof  38205  negpilt0  38232  xrgtso  38302  ioontr  38383  iccdifioo  38388  iccdifprioo  38389  fsummulc1f  38435  fsumiunss  38442  fnlimfvre2  38544  icccncfext  38573  dvcosre  38599  dvsinax  38601  ioodvbdlimc1lem2  38622  ioodvbdlimc2lem  38624  dvmptmulf  38627  dvnmul  38633  dvmptfprodlem  38634  dvnprodlem2  38637  stoweidlem1  38694  stoweidlem26  38719  stoweidlem34  38727  stoweidlem44  38737  stoweid  38756  stirlinglem5  38771  dirkercncflem1  38796  fourierdlem44  38844  fourierdlem56  38855  fourierdlem62  38861  fourierdlem89  38888  fourierdlem91  38890  fourierdlem100  38899  fourierdlem102  38901  fourierdlem103  38902  fourierdlem104  38903  fourierdlem108  38907  fourierdlem112  38911  fourierdlem114  38913  fouriersw  38924  rrndistlt  38986  gsumge0cl  39064  sge0tsms  39073  sge0ltfirpmpt2  39119  ovn0  39256  hoidmv1le  39284  hoidmvle  39290  ovnsubadd2lem  39335  ovolval4lem1  39339  vonioolem2  39372  smflimlem3  39459  nsssmfmbf  39465  axorbtnotaiffb  39519  axorbciffatcxorb  39521  abnotbtaxb  39531  fmtnoinf  39787  1nevenALTV  39941  nnsum3primes4  40005  tgblthelfgott  40030  tgoldbachlt  40031  tgblthelfgottOLD  40037  tgoldbachltOLD  40038  resisresindm  40131  residfi  40163  hashfxnn0  40215  upgrfi  40315  lfgrnloop  40348  lfuhgr1v0e  40478  vdegp1bi-av  40751  pthdlem2  40972  0ewlk  41280  0pth-av  41291  konigsbergiedgw  41414  konigsbergiedgwOLD  41415  konigsberglem1  41420  konigsberglem2  41421  konigsberglem3  41422  konigsberglem4  41423  konigsberglem5  41424  frgrwopreg2  41486  ldepslinc  42090  alimp-no-surprise  42295  aacllem  42315  amgmwlem  42316  amgmlemALT  42317
  Copyright terms: Public domain W3C validator