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

Theorem mpbi 208
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 194 . 2
41, 3ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  pm5.74i  245  notbii  296  pm5.19  360  ori  375  imori  413  pm4.71i  632  pm4.71ri  633  pm5.32i  637  pm3.24  882  pm5.16  890  biluk  933  4exmid  939  dn1  966  3ori  1288  trubifal  1434  cadan  1459  nic-dfim  1502  nic-dfneg  1503  nic-mp  1504  nic-mpALT  1505  tbw-negdf  1532  rb-imdf  1583  mpgbi  1621  19.35i  1689  19.36iv  1763  19.37iv  1769  19.36i  1965  ax6  2003  sbie  2149  sbieOLD  2150  sbidmOLD  2157  axi12  2433  bm1.1  2440  eqcomi  2470  eqtri  2486  eleqtri  2543  neii  2656  necomi  2727  nesymiOLD  2731  neeqtri  2755  neli  2792  nrex  2912  rexlimi  2939  rexlimiv  2943  isseti  3115  vtocl2  3162  vtocl3  3163  eueq1  3272  euxfr2  3284  cdeqri  3313  sseqtri  3535  3sstr3i  3541  pssn2lp  3604  equncomi  3649  unssi  3678  ssini  3720  unabs  3727  inabs  3728  dfin4  3737  npss0  3865  difid  3896  disjdif  3900  difin0  3901  snid  4057  iinrab2  4393  rintn0  4421  breqtri  4475  axsep  4572  bm1.3ii  4576  ax6vsep  4577  zfnuleu  4578  notzfaus  4627  zfpow  4631  dtru  4643  reusv2lem4  4656  reuxfr2d  4675  dtruALT  4684  dtruALT2  4696  op1stb  4722  copsexg  4737  copsexgOLD  4738  uniop  4755  pwundif  4792  onunisuci  4996  relop  5158  rn0  5259  dmresi  5334  issref  5385  somincom  5409  cnvcnv  5464  rescnvcnv  5475  cnvcnvres  5476  cnvsn  5496  cocnvcnv2  5524  cores2  5525  co01  5527  relcoi1  5541  cnviin  5549  iota4an  5575  fnopab  5710  mpt0  5713  fnmpti  5714  f1cnvcnv  5794  f1ovi  5857  eliman0  5900  fvco4i  5951  fmpti  6054  fvsnun2  6107  funiunfv  6160  oprabss  6388  relmptopab  6523  zfun  6593  tfinds2  6698  omon  6711  2nd0  6807  f1stres  6822  f2ndres  6823  relmpt2opab  6882  df1st2  6886  df2nd2  6887  fsplit  6905  reldmtpos  6982  dftpos4  6993  tpostpos  6994  tpos0  7004  smo0  7048  tfrlem14  7079  tfrlem16  7081  rdgsucg  7108  rdglimg  7110  frfnom  7119  oawordeulem  7222  uniixp  7512  dfdom2  7561  ssdomg  7581  xpcomf1o  7626  sbthlem5  7651  pwdom  7689  limensuci  7713  fiint  7817  fidomdm  7822  pwfilem  7834  mptfi  7839  fisn  7907  dffi3  7911  ordtypelem6  7969  ordtypelem7  7970  wemaplem2  7993  wdompwdom  8025  harwdom  8037  suc11reg  8057  zfinf  8077  axinf2  8078  noinfep  8097  cantnfvalf  8105  cantnflt  8112  cantnf0  8115  cantnf  8133  cantnfltOLD  8142  cantnfOLD  8155  tz9.1c  8182  tc2  8194  r111  8214  r1tr2  8216  r1ordg  8217  r1sssuc  8222  r1val1  8225  tz9.13  8230  r1elssi  8244  pwwf  8246  rankopb  8291  rankeq0b  8299  ranksuc  8304  rankmapu  8317  rankxplim  8318  rankxplim3  8320  rankxpsuc  8321  cp  8330  karden  8334  card0  8360  cardlim  8374  cardom  8388  infxpenlem  8412  alephsuc2  8482  alephgeom  8484  unialeph  8503  dfac4  8524  dfacacn  8542  cda1dif  8577  pm110.643  8578  infcda1  8594  ackbij1lem13  8633  ackbij2  8644  cf0  8652  cfsuc  8658  cfom  8665  cfslb2n  8669  ominf4  8713  fin23lem17  8739  fin23lem28  8741  fin23lem30  8743  fin23lem31  8744  fin23lem40  8752  isfin1-3  8787  dfacfin7  8800  fin1a2lem6  8806  itunitc1  8821  axcc3  8839  dcomex  8848  axdc2lem  8849  axcclem  8858  zfac  8861  ac3  8863  ackm  8866  axac2  8867  axac  8868  axaci  8869  cardeqv  8870  numth2  8872  numth  8873  brdom3  8927  fin71ac  8932  cardf  8946  aleph1  8967  cfpwsdom  8980  smobeth  8982  zfcndrep  9013  zfcndpow  9015  zfcndac  9018  gch2  9074  wunex3  9140  tskpr  9169  inar1  9174  rankcf  9176  tskcard  9180  tskuni  9182  grothpw  9225  axgroth4  9231  grothprim  9233  inaprc  9235  dmaddpi  9289  dmmulpi  9290  1lt2pi  9304  addpqf  9343  mulpqf  9345  1lt2nq  9372  supsrlem  9509  ssxr  9675  gtso  9687  subf  9845  negne0i  9917  negdiiOLD  9927  mulnzcnopr  10220  infmsup  10546  halflt1  10782  nn0ssz  10910  zeo  10973  numlt  11023  numltc  11024  uzf  11113  uzinfmi  11190  xaddf  11452  xsubge0  11482  xmulf  11493  infmxrcl  11537  infmxrlb  11554  infmxrgelb  11555  xrinfm0  11557  ixxf  11568  ixxssxr  11570  iooval2  11591  ioof  11651  unirnioo  11653  dfioo2  11654  fzval2  11704  fzf  11705  fz10  11735  fzpreddisj  11758  4fvwrd4  11822  fzof  11826  fzo0  11849  om2uzoi  12066  faclbnd4lem1  12371  hashkf  12407  hashgval  12408  hashinf  12410  hashresfn  12413  hashnn0n0nn  12458  hashbclem  12501  hashge3el3dif  12524  wrdexg  12557  rev0  12738  f1oun2prg  12865  sqrt2gt1lt2  13108  limsupgord  13295  limsupval  13297  fclim  13376  fsumrelem  13621  ackbijnn  13640  incexclem  13648  incexc  13649  arisum2  13672  georeclim  13681  geoisumr  13687  0.999...  13690  geoihalfsum  13691  ege2le3  13825  sin0  13884  ef01bndlem  13919  cos2bnd  13923  cos01gt0  13926  sincos2sgn  13929  sin4lt0  13930  rpnnen2lem3  13950  rpnnen2lem9  13956  rexpen  13961  cnso  13980  dvdslelem  14030  n2dvds1  14035  divalglem1  14052  divalglem5  14055  divalglem6  14056  divalglem10  14060  0bits  14089  sadcf  14103  sadcadd  14108  bitsshft  14125  smupf  14128  gcdf  14157  eucalgf  14212  2prm  14233  dfphi2  14304  pockthi  14425  prmreclem2  14435  prmrec  14440  vdwapf  14490  vdwap0  14494  vdwlem6  14504  ramval  14526  ramcl2lem  14527  karatsuba  14570  1259lem5  14617  2503lem3  14621  4001lem4  14626  structcnvcnv  14643  structfn  14645  strlemor1  14724  strleun  14727  prdsval  14852  prdsds  14861  imasdsfn  14911  imasdsval  14912  imasvscafn  14934  xpsc0  14957  xpsc1  14958  xpsff1o  14965  sscpwex  15184  wunfunc  15268  wunnat  15325  eldmcoa  15392  coapm  15398  catcfuccl  15436  catcxpccl  15476  yonedainv  15550  plusffval  15877  grpinvfvi  16091  mulgfvi  16146  symgsssg  16492  symgfisg  16493  psgnunilem5  16519  sylow3lem2  16648  oppglsm  16662  efgmf  16731  efgval  16735  efgsf  16747  0frgp  16797  gsumzaddlem  16934  gsumzaddlemOLD  16936  dmdprd  17029  dprdval  17034  dprdvalOLD  17036  invrfval  17322  drngui  17402  scaffval  17530  lssintcl  17610  mplsubrglem  18100  mplsubrglemOLD  18101  opsrtoslem2  18149  cnfld0  18442  cnfld1  18443  cnfldsub  18446  xrsds  18461  psgnghm  18616  zrhpsgnmhm  18620  recrng  18657  ipffval  18683  ocv1  18710  dsmmbas2  18768  mdetralt  19110  maducoeval2  19142  eltpsi  19447  unitg  19468  fctop  19505  cctop  19507  ppttop  19508  epttop  19510  leordtvallem1  19711  leordtvallem2  19712  iccordt  19715  iscnp2  19740  discmp  19898  concompcld  19935  1stcrestlem  19953  2ndcdisj  19957  topnlly  19992  disllycmp  19999  dis1stc  20000  txuni2  20066  xkotf  20086  dfac14lem  20118  prdstps  20130  txindis  20135  tx1stc  20151  xkohaus  20154  xkoptsub  20155  cnmpt1st  20169  cnmpt2nd  20170  ptcmpfi  20314  filcon  20384  trfil1  20387  fin1aufil  20433  tgpconcompeqg  20610  tgpconcomp  20611  tsmsresOLD  20645  tsmsres  20646  trust  20732  met1stc  21024  dscmet  21093  nmoval  21222  retopon  21270  cnfldtopon  21290  xrsxmet  21314  xrsmopn  21317  metdsval  21351  iimulcn  21438  icopnfhmeo  21443  iccpnfhmeo  21445  xrhmeo  21446  cnheiborlem  21454  lebnumii  21466  ishtpy  21472  htpycc  21480  pco1  21515  pcohtpylem  21519  pcopt  21522  pcopt2  21523  pcoass  21524  pcorevlem  21526  cfilresi  21734  rrxcph  21824  ovolval  21885  ovolf  21893  ovoliunlem3  21915  ovolicc1  21927  ovolicc2  21933  volf  21940  ioorf  21982  dyadf  22000  dyadmbl  22009  vitalilem5  22021  vitali  22022  mbfimaopnlem  22062  mbflimsup  22073  0plef  22079  i1fima  22085  i1fima2  22086  i1fd  22088  itg1ge0  22093  itg10  22095  i1f1lem  22096  i1fadd  22102  i1fmul  22103  i1fmulc  22110  mbfi1fseqlem5  22126  itg2addlem  22165  reldv  22274  dvbsss  22306  dvef  22381  lhop1lem  22414  deg1fvi  22485  plypf1  22609  coeeulem  22621  coeeu  22622  vieta1lem2  22707  aannenlem3  22726  aalioulem3  22730  dvradcnv  22816  pserulm  22817  pserdvlem2  22823  abelthlem6  22831  sinhalfpilem  22856  sincos4thpi  22906  tan4thpi  22907  sincos6thpi  22908  pige3  22910  resinf1o  22923  tanord1  22924  tanregt0  22926  efabl  22937  relogrn  22949  dfrelog  22953  logneg  22972  logltb  22984  logcn  23028  logf1o2  23031  dvlog  23032  efopnlem2  23038  efopn  23039  logccv  23044  dvsqrt  23118  cxpcn3  23122  angpined  23161  1cubr  23173  asinsin  23223  asin1  23225  reasinsin  23227  atan0  23239  atanbnd  23257  atan1  23259  log2cnv  23275  log2ublem3  23279  log2ub  23280  birthday  23284  amgmlem  23319  emcllem5  23329  emgt0  23336  harmonicbnd3  23337  ftalem3  23348  basellem4  23357  sgmf  23419  ppi1  23438  cht1  23439  vma1  23440  ppiltx  23451  sqff1o  23456  ppiublem1  23477  ppiublem2  23478  ppiub  23479  chtub  23487  dchreq  23533  bposlem7  23565  bposlem8  23566  bposlem9  23567  lgsdir2lem2  23599  lgsdir2lem3  23600  chebbnd1  23657  chto1ub  23661  chpo1ubb  23666  pntibndlem1  23774  tgldimor  23893  tglnfn  23934  axlowdimlem4  24248  axlowdimlem16  24260  axlowdim  24264  umgrafi  24322  usgraexmpl  24401  usgraexmplc  24404  usgrafilem1  24411  2trllemA  24552  wlkntrllem1  24561  wlkntrllem3  24563  0pth  24572  spthispth  24575  2pthon  24604  2pthon3v  24606  constr3trllem3  24652  constr3pthlem3  24657  konigsberg  24987  frgrawopreg2  25051  ex-dif  25144  ex-un  25145  ex-in  25146  ex-fl  25168  avril1  25171  ginvsn  25351  cnid  25353  mulid  25358  rngosn3  25428  vcoprnelem  25471  vcex  25473  cnnvm  25588  ipasslem8  25752  ipasslem10  25754  hvsubf  25932  normlem1  26027  normlem6  26032  normlem7  26033  norm-ii-i  26054  norm3adifii  26065  hilid  26078  hlimf  26155  hhssabloi  26178  hhssnv  26180  hhshsslem1  26183  shincli  26280  shsval2i  26305  shs0i  26367  chj0i  26373  chm1i  26374  chincli  26378  chdmm1i  26395  shjshsi  26410  chsup0  26466  h1de2bi  26472  spansnpji  26496  cmcmlem  26509  cmcmii  26515  cmcm2ii  26516  cmcm3ii  26517  pjidmi  26591  pjssmii  26599  pj0i  26611  pjocini  26616  mayetes3i  26648  df0op2  26671  hoaddcomi  26691  hoaddassi  26695  hocadddiri  26698  hocsubdiri  26699  hoaddid1i  26705  ho0coi  26707  hoid1i  26708  hoid1ri  26709  hodseqi  26713  honegsubi  26715  adj1o  26813  hoddii  26908  lnopunilem1  26929  lnopunilem2  26930  nmcopexi  26946  nmcopex  26948  nmcoplb  26949  nmcfnexi  26970  nmcfnex  26972  nmcfnlb  26973  adjbd1o  27004  adjcoi  27019  nmopcoadji  27020  opsqrlem6  27064  pjsdii  27074  pjddii  27075  pjidmcoi  27096  pjtoi  27098  pjin1i  27111  pjclem1  27114  stji1i  27161  reuxfr3d  27388  inindif  27414  iuninc  27428  fnresin  27470  rinvf1o  27472  suppss2f  27477  xppreima  27487  ofoprabco  27505  funcnvmptOLD  27509  gtiso  27519  df1stres  27522  df2ndres  27523  snct  27534  dmct  27537  ffsrn  27552  fpwrelmapffs  27557  xrge0infssd  27581  nnindf  27610  nn0min  27611  ressplusf  27638  xrsclat  27668  xrge0base  27673  xrge00  27674  xrge0neqmnf  27679  xrnarchi  27728  xrge0slmod  27834  locfinreflem  27843  locfinref  27844  unicls  27885  sqsscirc1  27890  mhmhmeotmd  27909  rmulccn  27910  raddcn  27911  xrge0iifiso  27917  xrge0iifhmeo  27918  lmxrge0  27934  cnzh  27951  rezh  27952  qqh0  27965  qqh1  27966  qqhre  27998  rnlogblem  28015  log2le1  28023  esumnul  28059  esum0  28060  esumsn  28072  esumpfinvallem  28080  esumpfinvalf  28082  esumpcvgval  28084  sigaclfu2  28121  dmsigagen  28144  ddemeas  28208  imambfm  28233  mbfmvolf  28237  br2base  28240  omsfval  28265  oms0  28266  sibfof  28282  sitg0  28288  eulerpartlemt  28310  eulerpartgbij  28311  0rrv  28390  coinfliplem  28417  coinflipprob  28418  coinfliprv  28421  ballotlem2  28427  ballotlem4  28437  ballotlem5  28438  ballotlemi1  28441  ballotlem7  28474  ballotth  28476  signsplypnf  28507  signsply0  28508  signsw0g  28513  signswch  28518  signsvf0  28537  subfacf  28619  subfacp1lem1  28623  subfacp1lem5  28628  subfacp1lem6  28629  subfacval3  28633  erdszelem2  28636  kur14lem4  28653  iooscon  28692  iccllyscon  28695  msrfo  28906  mthmpps  28942  problem5  29023  quad3  29024  ghomgrpilem1  29025  ghomgrpilem2  29026  circum  29040  axextprim  29073  axrepprim  29074  axunprim  29075  axinfprim  29078  axacprim  29079  inffz  29108  logi  29121  risefall0lem  29148  setinds  29210  dfon2lem2  29216  dfon2lem4  29218  axextdfeq  29230  poseq  29333  wfrlem4  29346  frrlem4  29390  nosgnn0  29418  sltsolem1  29428  bdayfo  29435  symdifV  29475  fobigcup  29550  snelsingles  29572  fullfunfnv  29596  fullfunfv  29597  rankaltopb  29629  rank0  29827  rankeq1o  29828  hfuni  29841  nabi1i  29857  nabi2i  29858  limsucncmpi  29910  tan2h  30047  mblfinlem1  30051  mblfinlem2  30052  ovoliunnfl  30056  voliunnfl  30058  dvtanlem  30064  itg2addnclem  30066  itg2addnclem2  30067  dvcnsqrt  30101  asindmre  30102  areacirclem1  30107  fneer  30171  neibastop1  30177  fdc  30238  cntotbnd  30292  heiborlem6  30312  rrnval  30323  reheibor  30335  prter2  30622  diophrw  30692  rabren3dioph  30749  pellexlem6  30770  pellex  30771  frmx  30849  frmy  30850  jm2.23  30938  jm2.27dlem3  30953  axac10  30975  pw2f1ocnv  30979  kelac2lem  31010  lmhmlnmsplit  31033  pwfi2f1o  31044  frlmpwfi  31046  seff  31189  expgrowthi  31238  expgrowth  31240  binomcxplemnotnn0  31261  negpilt0  31462  ioontr  31549  iccdifioo  31555  iccdifprioo  31556  fsummulc1f  31569  icccncfext  31690  dvcosre  31706  dvsinax  31708  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvmptmulf  31734  dvnmul  31740  dvmptfprodlem  31741  dvnprodlem2  31744  stoweidlem1  31783  stoweidlem26  31808  stoweidlem34  31816  stoweidlem44  31826  stoweid  31845  stirlinglem5  31860  dirkercncflem1  31885  fourierdlem44  31933  fourierdlem56  31945  fourierdlem62  31951  fourierdlem89  31978  fourierdlem91  31980  fourierdlem100  31989  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem108  31997  fourierdlem112  32001  fourierdlem114  32003  fouriersw  32014  axorbtnotaiffb  32098  axorbciffatcxorb  32100  abnotbtaxb  32111  resisresindm  32305  residfi  32314  ldepslinc  33110  alimp-no-surprise  33196  aacllem  33216  ee233  33289  ax6e2nd  33331  in1  33348  dfvd2ani  33360  dfvd2i  33362  dfvd3i  33369  dfvd3ani  33372  e0bi  33573  uun2221  33610  uun2221p1  33611  uun2221p2  33612  en3lpVD  33645  relopabVD  33701  ax6e2ndVD  33708  ax6e2ndALT  33730  bnj521  33792  bnj1098  33842  bnj1109  33845  bnj1131  33846  bnj1533  33910  bnj151  33935  bnj580  33971  bnj852  33979  bnj864  33980  bnj865  33981  bnj978  34007  bnj1021  34022  bnj907  34023  bnj1093  34036  bnj1145  34049  bnj1172  34057  bnj1174  34059  bnj1176  34061  bnj1186  34063  bj-nfxfr  34218  bj-axsep  34379  bj-zfpow  34381  bj-dtru  34383  bj-n0i  34503  bj-snsetex  34521  bj-tagss  34538  bj-2upln0  34581  bj-2upln1upl  34582  bj-nuliota  34586  bj-elid  34599  bj-pinftyccb  34624  bj-minftyccb  34628  bj-pinftynminfty  34630  renegclALT  34694  mapdunirnN  37377  trclubg  37785  0heALT  37806  frege54cor1a  37891  int-rightdistd  38001  int-sqdefd  38002  int-sqgeq0d  38007
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 185
  Copyright terms: Public domain W3C validator