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

Theorem mpbi 221
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 207 . 2 (𝜑𝜓)
41, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wb 197
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 198
This theorem is referenced by:  pm5.74i  262  notbii  311  pm5.19  376  pm3.24  391  pm4.71i  551  pm4.71ri  552  pm5.32i  566  imori  872  ori  879  pm5.16  1028  biluk  1041  4exmidOLD  1067  dn1  1073  3ori  1541  cadan  1703  nic-dfim  1749  nic-dfneg  1750  nic-mp  1751  nic-mpALT  1752  tbw-negdf  1779  rb-imdf  1830  nfri  1869  mpgbi  1880  19.35i  1968  19.36ivOLD  2085  19.37ivOLD  2091  nfim1  2233  19.36i  2268  ax6  2427  sbie  2569  datisi  2759  disamis  2761  dimatis  2770  fresison  2772  bamalip  2778  axi12  2793  bm1.1OLD  2801  nulmo  2802  eqcomi  2826  eqtri  2839  eleqtri  2894  neii  2991  necomi  3043  neeqtri  3061  neli  3094  nrex  3198  rexlimi  3223  rexlimiv  3226  isseti  3414  vtocl2  3465  vtocl3  3466  eueqi  3588  euxfr2  3600  cdeqri  3630  sseqtri  3845  3sstr3i  3851  pssn2lp  3917  equncomi  3969  unssi  3998  ssini  4043  unabs  4067  inabs  4068  dfin4  4080  difid  4160  ab0orv  4165  disjdif  4247  difin0  4248  snid  4413  rabrsn  4461  iinrab2  4786  symdifv  4801  rintn0  4822  breqtri  4880  axsep  4987  bm1.3ii  4991  ax6vsep  4992  zfnuleuOLD  4993  notzfaus  5045  zfpow  5049  dtru  5053  dtruALT  5070  reusv2lem4  5083  reuxfr2d  5101  dtruALT2  5114  op1stb  5142  copsexg  5158  uniop  5183  pwundif  5229  rn0  5591  dmresi  5682  idrefOLD  5733  somincom  5754  cnvcnv  5810  cnvcnvOLD  5811  rescnvcnv  5821  cnvcnvres  5822  cnvsnOLD  5845  cocnvcnv2  5874  cores2  5875  co01  5877  cnviin  5899  onunisuci  6063  iota4an  6092  fnopab  6238  mpt0  6241  fnmpti  6242  f1cnvcnv  6334  f1ovi  6400  eliman0  6452  fvco4i  6506  fmpti  6613  fvsnun2  6683  funiunfv  6739  oprabss  6985  relmptopab  7122  zfun  7189  tfinds2  7302  omon  7315  2nd0  7414  f1stres  7431  f2ndres  7432  cnvoprab  7471  relmpt2opab  7502  df1st2  7506  df2nd2  7507  fsplit  7525  reldmtpos  7604  dftpos4  7615  tpostpos  7616  tpos0  7626  wfrlem4  7662  wfrlem4OLD  7663  smo0  7700  tfrlem14  7732  tfrlem16  7734  rdgsucg  7764  rdglimg  7766  frfnom  7775  oawordeulem  7880  uniixp  8177  dfdom2  8227  ssdomg  8247  xpcomf1o  8297  sbthlem5  8322  pwdom  8360  limensuci  8384  fiint  8485  fidomdm  8491  residfi  8495  pwfilem  8508  mptfi  8513  fisn  8581  dffi3  8585  ordtypelem6  8676  ordtypelem7  8677  wemaplem2  8700  wdompwdom  8731  harwdom  8743  suc11reg  8772  zfinf  8792  axinf2  8793  noinfep  8813  cantnfvalf  8818  cantnflt  8825  cantnf0  8828  cantnf  8846  tz9.1c  8862  tc2  8874  r111  8894  r1tr2  8896  r1ordg  8897  r1sssuc  8902  r1val1  8905  tz9.13  8910  r1elssi  8924  pwwf  8926  rankopb  8971  rankeq0b  8979  ranksuc  8984  rankmapu  8997  rankxplim  8998  rankxplim3  9000  rankxpsuc  9001  cp  9010  karden  9014  card0  9076  cardlim  9090  cardom  9104  infxpenlem  9128  alephsuc2  9195  alephgeom  9197  unialeph  9216  dfac4  9237  dfacacn  9257  cda1dif  9292  pm110.643  9293  infcda1  9309  ackbij1lem13  9348  ackbij2  9359  cf0  9367  cfsuc  9373  cfom  9380  cfslb2n  9384  ominf4  9428  fin23lem17  9454  fin23lem28  9456  fin23lem30  9458  fin23lem31  9459  fin23lem40  9467  isfin1-3  9502  dfacfin7  9515  fin1a2lem6  9521  itunitc1  9536  axcc3  9554  dcomex  9563  axdc2lem  9564  axcclem  9573  zfac  9576  ac3  9578  ackm  9581  axac2  9582  axac  9583  axaci  9584  cardeqv  9585  numth2  9587  numth  9588  dmct  9640  brdom3  9644  fin71ac  9649  cardf  9666  aleph1  9687  cfpwsdom  9700  smobeth  9702  zfcndrep  9730  zfcndpow  9732  zfcndac  9735  gch2  9791  wunex3  9857  tskpr  9886  inar1  9891  rankcf  9893  tskcard  9897  tskuni  9899  grothpw  9942  axgroth4  9948  grothprim  9950  inaprc  9952  dmaddpi  10006  dmmulpi  10007  1lt2pi  10021  addpqf  10060  mulpqf  10062  1lt2nq  10089  supsrlem  10226  ssxr  10401  gtso  10413  subf  10577  negne0i  10650  mulnzcnopr  10967  infrenegsup  11300  halflt1  11536  nn0ssz  11683  3halfnz  11741  zeo  11748  numlt  11803  numltc  11804  le9lt10  11805  decle  11812  uzf  11926  xaddf  12292  xsubge0  12328  xmulf  12339  ixxf  12422  ixxssxr  12424  iooval2  12445  ioof  12509  unirnioo  12511  dfioo2  12512  xrge0neqmnfOLD  12515  fzval2  12571  fzf  12572  0nelfz1  12602  fz10  12604  fzpreddisj  12632  4fvwrd4  12702  fzof  12710  fzo0  12735  fldiv4p1lem1div2  12879  fldiv4lem1div2  12881  om2uzoi  12997  faclbnd4lem1  13319  hashkf  13358  hashgval  13359  hashinf  13361  hashresfn  13367  hashnn0n0nn  13417  hashbclem  13472  hashge3el3dif  13504  wrdexg  13545  rev0  13756  f1oun2prg  13905  trclublem  13978  sqrt2gt1lt2  14257  limsupgord  14445  fclim  14526  fsumrelem  14780  ackbijnn  14801  incexclem  14809  incexc  14810  arisum2  14834  georeclim  14844  geoisumr  14850  0.999...  14853  risefall0lem  14996  ege2le3  15059  sin0  15118  ef01bndlem  15153  cos2bnd  15157  cos01gt0  15160  sincos2sgn  15163  sin4lt0  15164  rpnnen2lem3  15184  rpnnen2lem9  15190  rexpen  15196  cnso  15215  dvdslelem  15273  n2dvds1  15343  divalglem1  15356  divalglem5  15359  divalglem6  15360  divalglem10  15364  flodddiv4  15375  0bits  15399  sadcf  15413  sadcadd  15418  bitsshft  15435  smupf  15438  gcdf  15472  eucalgf  15534  2prm  15642  dfphi2  15715  pockthi  15847  prmrec  15862  vdwapf  15912  vdwap0  15916  vdwlem6  15926  karatsuba  16024  1259lem5  16072  2503lem3  16076  4001lem4  16081  structcnvcnv  16101  structfn  16104  strlemor1OLD  16199  strleun  16202  prdsval  16339  prdsds  16348  imasvscafn  16421  xpsc0  16444  xpsc1  16445  xpsff1o  16452  sscpwex  16698  wunfunc  16782  wunnat  16839  eldmcoa  16938  coapm  16944  catcfuccl  16982  catcxpccl  17071  yonedainv  17145  plusffval  17471  grpinvfvi  17687  mulgfvi  17769  symgsssg  18107  symgfisg  18108  psgnunilem5  18134  sylow3lem2  18263  oppglsm  18277  efgmf  18346  efgval  18350  efgsf  18362  0frgp  18412  dmdprd  18618  dprdval  18623  invrfval  18894  drngui  18976  scaffval  19104  rmodislmod  19154  lssintcl  19190  mplsubrglem  19667  opsrtoslem2  19712  cnfldfun  19985  cnfld0  19997  cnfld1  19998  cnfldsub  20001  xrsds  20016  psgnghm  20152  zrhpsgnmhm  20156  recrng  20195  ipffval  20222  ocv1  20253  dsmmbas2  20311  mdetralt  20645  maducoeval2  20677  eltpsi  20982  unitg  21005  fctop  21042  cctop  21044  ppttop  21045  epttop  21047  leordtvallem1  21248  leordtvallem2  21249  iccordt  21252  iscnp2  21277  discmp  21435  conncompcld  21471  1stcrestlem  21489  2ndcdisj  21493  topnlly  21528  disllycmp  21535  dis1stc  21536  txuni2  21602  xkotf  21622  dfac14lem  21654  prdstps  21666  txindis  21671  tx1stc  21687  xkohaus  21690  xkoptsub  21691  cnmpt1st  21705  cnmpt2nd  21706  ptcmpfi  21850  trfil1  21923  fin1aufil  21969  tgpconncompeqg  22148  tgpconncomp  22149  tsmsres  22180  trust  22266  met1stc  22559  dscmet  22610  retopon  22800  cnfldtopon  22819  xrsxmet  22845  xrsmopn  22848  iimulcn  22970  icopnfhmeo  22975  iccpnfhmeo  22977  xrhmeo  22978  cnheiborlem  22986  lebnumii  22998  ishtpy  23004  htpycc  23012  pco1  23047  pcohtpylem  23051  pcopt  23054  pcopt2  23055  pcoass  23056  pcorevlem  23058  cfilresi  23326  rrxcph  23414  ovoliunlem3  23507  ovolicc1  23519  ovolicc2  23525  volf  23532  ioorf  23576  dyadf  23594  dyadmbl  23603  vitalilem5  23615  vitali  23616  mbfimaopnlem  23658  mbflimsup  23669  0plef  23675  i1fima  23681  i1fima2  23682  i1fd  23684  itg1ge0  23689  itg10  23691  i1f1lem  23692  i1fadd  23698  i1fmul  23699  i1fmulc  23706  mbfi1fseqlem5  23722  itg2addlem  23761  reldv  23870  dvbsss  23902  dvef  23979  lhop1lem  24012  deg1fvi  24081  plypf1  24204  coeeulem  24216  coeeu  24217  vieta1lem2  24302  aannenlem3  24321  aalioulem3  24325  dvradcnv  24411  pserulm  24412  pserdvlem2  24418  abelthlem6  24426  sinhalfpilem  24452  sincos4thpi  24502  tan4thpi  24503  sincos6thpi  24504  pige3  24506  resinf1o  24519  tanord1  24520  tanregt0  24522  efabl  24533  relogrn  24544  dfrelog  24548  logneg  24570  logltb  24582  logcn  24629  logf1o2  24632  dvlog  24633  efopnlem2  24639  efopn  24640  logccv  24645  dvsqrt  24719  dvcnsqrt  24721  cxpcn3  24725  logblog  24766  angpined  24793  1cubr  24805  asinsin  24855  asin1  24857  reasinsin  24859  atan0  24871  atanbnd  24889  atan1  24891  log2cnv  24907  log2ub  24912  log2le1  24913  birthday  24917  amgmlem  24952  emcllem5  24962  emgt0  24969  harmonicbnd3  24970  ftalem3  25037  basellem4  25046  sgmf  25107  ppi1  25126  cht1  25127  vma1  25128  ppiltx  25139  sqff1o  25144  ppiublem1  25163  ppiublem2  25164  ppiub  25165  chtub  25173  dchreq  25219  bposlem7  25251  bposlem8  25252  bposlem9  25253  lgsdir2lem2  25287  lgsdir2lem3  25288  chebbnd1  25397  chto1ub  25401  chpo1ubb  25406  pntibndlem1  25514  tgldimor  25633  tglnfn  25678  axlowdimlem4  26061  axlowdimlem16  26073  axlowdim  26077  upgrfi  26222  lfgrnloop  26256  lfuhgr1v0e  26384  usgrexmplef  26389  usgrres  26438  vdegp1bi  26683  vtxdginducedm1lem2  26686  pthdlem2  26914  wpthswwlks2on  27124  0ewlk  27309  0pth  27320  konigsbergiedgw  27443  konigsberglem1  27447  konigsberglem2  27448  konigsberglem3  27449  konigsberglem4  27450  konigsberglem5  27451  ex-dif  27633  ex-un  27634  ex-in  27635  ex-fl  27657  avril1  27672  n0lplig  27688  vcex  27783  cnidOLD  27787  cnnvm  27887  ipasslem8  28042  ipasslem10  28044  hvsubf  28222  normlem1  28317  normlem6  28322  normlem7  28323  norm-ii-i  28344  norm3adifii  28355  hilid  28368  hlimf  28444  hhssabloi  28469  hhssnv  28471  hhshsslem1  28474  shincli  28571  shsval2i  28596  shs0i  28658  chj0i  28664  chm1i  28665  chincli  28669  chdmm1i  28686  shjshsi  28701  chsup0  28757  h1de2bi  28763  spansnpji  28787  cmcmlem  28800  cmcmii  28806  cmcm2ii  28807  cmcm3ii  28808  pjidmi  28882  pjssmii  28890  pj0i  28902  pjocini  28907  mayetes3i  28938  df0op2  28961  hoaddcomi  28981  hoaddassi  28985  hocadddiri  28988  hocsubdiri  28989  hoaddid1i  28995  ho0coi  28997  hoid1i  28998  hoid1ri  28999  hodseqi  29003  honegsubi  29005  adj1o  29103  hoddii  29198  lnopunilem1  29219  lnopunilem2  29220  nmcopexi  29236  nmcopex  29238  nmcoplb  29239  nmcfnexi  29260  nmcfnex  29262  nmcfnlb  29263  adjbd1o  29294  adjcoi  29309  nmopcoadji  29310  opsqrlem6  29354  pjsdii  29364  pjddii  29365  pjidmcoi  29386  pjtoi  29388  pjin1i  29401  pjclem1  29404  stji1i  29451  reuxfr3d  29677  inindif  29700  iuninc  29726  fnresin  29779  rinvf1o  29781  suppss2f  29788  xppreima  29798  ofoprabco  29813  funcnvmptOLD  29816  gtiso  29827  df1stres  29830  df2ndres  29831  snct  29840  padct  29846  ffsrn  29853  fpwrelmapffs  29858  nnindf  29914  nn0min  29916  dp2lt  29940  dp2ltsuc  29941  dp2ltc  29942  dplti  29960  dpmul  29968  dpmul4  29969  ressplusf  29997  xrsclat  30027  xrge0base  30032  xrge00  30033  xrnarchi  30085  xrge0slmod  30191  locfinreflem  30254  locfinref  30255  unicls  30296  sqsscirc1  30301  mhmhmeotmd  30320  rmulccn  30321  raddcn  30322  xrge0iifiso  30328  xrge0iifhmeo  30329  lmxrge0  30345  cnzh  30361  rezh  30362  qqh0  30375  qqh1  30376  qqhre  30411  rrhre  30412  esumnul  30457  esum0  30458  esumsnf  30473  esumpfinvallem  30483  esumpfinvalf  30485  esumpcvgval  30487  esumcvgsum  30497  esumsup  30498  esumcvgre  30500  sigaclfu2  30531  dmsigagen  30554  ldgenpisyslem1  30573  ddemeas  30646  imambfm  30671  mbfmvolf  30675  br2base  30678  omssubadd  30709  sibfof  30749  sitg0  30755  eulerpartlemt  30780  eulerpartgbij  30781  0rrv  30860  coinfliplem  30887  coinflipprob  30888  coinfliprv  30891  ballotlem2  30897  ballotlem4  30907  ballotlem5  30908  ballotlemi1  30911  ballotlem7  30944  ballotth  30946  signsplypnf  30974  signsply0  30975  signsw0g  30980  signswch  30985  signsvf0  31004  hashreprin  31045  reprfz1  31049  chtvalz  31054  hgt750lemd  31073  hgt750lem  31076  hgt750lem2  31077  bnj521  31150  bnj1098  31198  bnj1109  31201  bnj1131  31202  bnj1533  31266  bnj151  31291  bnj580  31327  bnj852  31335  bnj864  31336  bnj865  31337  bnj978  31363  bnj1021  31378  bnj907  31379  bnj1093  31392  bnj1145  31405  bnj1172  31413  bnj1174  31415  bnj1176  31417  bnj1186  31419  subfacf  31501  subfacp1lem1  31505  subfacp1lem5  31510  subfacp1lem6  31511  subfacval3  31515  erdszelem2  31518  kur14lem4  31535  ioosconn  31573  iccllysconn  31576  msrfo  31787  mthmpps  31823  problem5  31906  quad3  31907  circum  31911  axextprim  31921  axrepprim  31922  axunprim  31923  axinfprim  31926  axacprim  31927  inffzOLD  31958  logi  31963  bcneg1  31965  setinds  32024  dfon2lem2  32030  dfon2lem4  32032  axextdfeq  32044  poseq  32095  frrlem4  32125  nosgnn0  32153  sltsolem1  32168  bdayfo  32170  nolt02o  32187  noetalem3  32207  dmscut  32260  fobigcup  32349  snelsingles  32371  fullfunfnv  32395  fullfunfv  32396  rankaltopb  32428  rank0  32619  rankeq1o  32620  hfuni  32633  fneer  32690  neibastop1  32696  nabi1i  32731  nabi2i  32732  limsucncmpi  32782  knoppcnlem8  32828  knoppcnlem11  32831  cnndvlem1  32866  bj-consensusALT  32899  bj-axsep  33125  bj-zfpow  33127  bj-dtru  33129  bj-sbidmOLD  33162  bj-n0i  33264  bj-snsetex  33279  bj-tagss  33296  bj-2upln0  33339  bj-2upln1upl  33340  bj-nuliota  33347  bj-0int  33384  bj-elid  33419  bj-pinftyccb  33443  bj-minftyccb  33447  bj-pinftynminfty  33449  f1omptsnlem  33518  mptsnunlem  33520  topdifinffinlem  33529  relowlpssretop  33546  1oequni2o  33550  cnfinltrel  33575  imadifss  33715  tan2h  33732  poimirlem3  33743  poimirlem9  33749  poimirlem16  33756  poimirlem17  33757  poimirlem18  33758  poimirlem19  33759  poimirlem20  33760  poimirlem22  33762  poimirlem30  33770  mblfinlem1  33777  mblfinlem2  33778  ovoliunnfl  33782  voliunnfl  33784  itg2addnclem  33791  itg2addnclem2  33792  asindmre  33825  areacirclem1  33830  fdc  33870  cntotbnd  33924  heiborlem6  33944  rrnval  33955  reheibor  33967  rngosn3  34052  ineqcomi  34345  cnvresrn  34447  moantr  34458  inxp2  34460  dfxrn2  34469  cnvcosseq  34523  refrelcosslem  34543  1cosscnvxrn  34556  prter2  34678  renegclALT  34760  mapdunirnN  37448  rntrclfvOAI  37773  diophrw  37841  rabren3dioph  37898  pellexlem6  37917  pellex  37918  frmx  37996  frmy  37997  jm2.23  38081  jm2.27dlem3  38096  axac10  38118  pw2f1ocnv  38122  kelac2lem  38152  lmhmlnmsplit  38175  pwfi2f1o  38184  frlmpwfi  38186  ifpbiidcor  38336  cnvnonrel  38411  rnnonrel  38414  resnonrel  38415  cononrel1  38417  cononrel2  38418  fvnonrel  38420  cnvcnvintabd  38423  cnvintabd  38426  rclexi  38439  rtrclex  38441  clcnvlem  38447  cnvrcl0  38449  dmtrcl  38451  rntrcl  38452  dfrtrcl5  38453  iunrelexp0  38511  dmtrclfvRP  38539  rntrclfv  38541  corcltrcl  38548  cotrclrcl  38551  0heALT  38594  frege54cor1a  38675  dssmapnvod  38831  uneqsn  38838  clsk3nimkb  38855  gneispace  38949  int-sqdefd  39001  int-sqgeq0d  39006  seff  39025  expgrowthi  39049  expgrowth  39051  binomcxplemnotnn0  39072  ee233  39240  ax6e2nd  39289  in1  39302  dfvd2ani  39314  dfvd2i  39316  dfvd3i  39323  dfvd3ani  39326  e0bi  39517  uun2221  39554  uun2221p1  39555  uun2221p2  39556  en3lpVD  39591  relopabVD  39648  ax6e2ndVD  39655  ax6e2ndALT  39677  pssnssi  39792  nnf1oxpnn  39890  icof  39915  negpilt0  39991  xrgtso  40058  supxrleubrnmptf  40176  xrpnf  40212  ioontr  40235  iccdifioo  40239  iccdifprioo  40240  uzinico2  40286  fsummulc1f  40299  fsumiunss  40304  fnlimfvre2  40406  limsupreuz  40466  limsupvaluz2  40467  limsup10ex  40502  icccncfext  40597  dvcosre  40623  dvsinax  40624  ioodvbdlimc1lem2  40644  ioodvbdlimc2lem  40646  dvmptmulf  40649  dvnmul  40655  dvmptfprodlem  40656  dvnprodlem2  40659  stoweidlem1  40714  stoweidlem26  40739  stoweidlem34  40747  stoweidlem44  40757  stoweid  40776  stirlinglem5  40791  dirkercncflem1  40816  fourierdlem44  40864  fourierdlem56  40875  fourierdlem62  40881  fourierdlem89  40908  fourierdlem91  40910  fourierdlem100  40919  fourierdlem102  40921  fourierdlem103  40922  fourierdlem104  40923  fourierdlem108  40927  fourierdlem112  40931  fourierdlem114  40933  fouriersw  40944  rrndistlt  41006  gsumge0cl  41084  sge0tsms  41093  sge0ltfirpmpt2  41139  ovn0  41279  hoidmv1le  41307  hoidmvle  41313  ovnsubadd2lem  41358  ovolval4lem1  41362  vonioolem2  41394  smflimlem3  41480  nsssmfmbf  41486  axorbtnotaiffb  41569  axorbciffatcxorb  41571  abnotbtaxb  41581  euabsneu  41669  fmtnoinf  42040  1nevenALTV  42194  nnsum3primes4  42268  tgblthelfgott  42295  tgoldbachlt  42296  sprval  42314  ldepslinc  42883  alimp-no-surprise  43115  aacllem  43135  amgmwlem  43136  amgmlemALT  43137
  Copyright terms: Public domain W3C validator