MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbi Structured version   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  |-  ph
mpbi.maj  |-  ( ph  <->  ps )
Assertion
Ref Expression
mpbi  |-  ps

Proof of Theorem mpbi
StepHypRef Expression
1 mpbi.min . 2  |-  ph
2 mpbi.maj . . 3  |-  ( ph  <->  ps )
32biimpi 194 . 2  |-  ( ph  ->  ps )
41, 3ax-mp 5 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184
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
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  877  pm5.16  885  biluk  924  4exmid  930  dn1  957  3ori  1278  trubifal  1408  cadan  1433  nic-dfim  1476  nic-dfneg  1477  nic-mp  1478  nic-mpALT  1479  tbw-negdf  1506  rb-imdf  1557  mpgbi  1594  19.35i  1656  19.36i  1893  19.37aiv  1919  ax6  1947  sbie  2100  sbieOLD  2101  sbcoOLD  2107  sbidmOLD  2110  axi12  2417  eqcomi  2442  eqtri  2458  eleqtri  2510  neii  2605  neeqtri  2624  nesymi  2643  necomi  2689  neli  2702  nrex  2813  rexlimi  2829  isseti  2973  vtocl2  3020  vtocl3  3021  eueq1  3127  euxfr2  3139  cdeqri  3167  sseqtri  3383  3sstr3i  3389  pssn2lp  3452  equncomi  3497  unssi  3526  ssini  3568  unabs  3575  inabs  3576  dfin4  3585  npss0  3712  difid  3742  disjdif  3746  difin0  3747  snid  3900  iinrab2  4228  rintn0  4256  breqtri  4310  axsep  4407  bm1.3ii  4411  ax6vsep  4412  zfnuleu  4413  notzfaus  4462  zfpow  4466  dtru  4478  reusv2lem4  4491  reuxfr2d  4510  dtruALT  4519  dtruALT2  4531  op1stb  4557  copsexg  4571  copsexgOLD  4572  uniop  4589  pwundif  4623  onunisuci  4827  relop  4985  rn0  5086  dmresi  5156  issref  5206  somincom  5230  cnvcnv  5285  rescnvcnv  5296  cnvcnvres  5297  cnvsn  5317  cocnvcnv2  5344  cores2  5345  co01  5347  relcoi1  5361  cnviin  5369  iota4an  5395  fnopab  5530  mpt0  5533  fnmpti  5534  f1cnvcnv  5609  f1ovi  5672  eliman0  5714  fvco4i  5764  fmpti  5861  fvsnun2  5909  funiunfv  5960  oprabss  6171  relmptopab  6303  zfun  6368  tfinds2  6469  omon  6482  2nd0  6579  f1stres  6593  f2ndres  6594  relmpt2opab  6650  df1st2  6654  df2nd2  6655  fsplit  6672  reldmtpos  6748  dftpos4  6759  tpostpos  6760  tpos0  6770  smo0  6811  tfrlem14  6842  tfrlem16  6844  rdgsucg  6871  rdglimg  6873  frfnom  6882  oawordeulem  6985  uniixp  7278  dfdom2  7327  ssdomg  7347  xpcomf1o  7392  sbthlem5  7417  pwdom  7455  limensuci  7479  fiint  7580  fidomdm  7585  pwfilem  7597  mptfi  7602  fisn  7669  dffi3  7673  ordtypelem6  7729  ordtypelem7  7730  wemaplem2  7753  wdompwdom  7785  harwdom  7797  suc11reg  7817  zfinf  7837  axinf2  7838  noinfep  7857  cantnfvalf  7865  cantnflt  7872  cantnf0  7875  cantnf  7893  cantnfltOLD  7902  cantnfOLD  7915  tz9.1c  7942  tc2  7954  r111  7974  r1tr2  7976  r1ordg  7977  r1sssuc  7982  r1val1  7985  tz9.13  7990  r1elssi  8004  pwwf  8006  rankopb  8051  rankeq0b  8059  ranksuc  8064  rankmapu  8077  rankxplim  8078  rankxplim3  8080  rankxpsuc  8081  cp  8090  karden  8094  card0  8120  cardlim  8134  cardom  8148  infxpenlem  8172  alephsuc2  8242  alephgeom  8244  unialeph  8263  dfac4  8284  dfacacn  8302  cda1dif  8337  pm110.643  8338  infcda1  8354  ackbij1lem13  8393  ackbij2  8404  cf0  8412  cfsuc  8418  cfom  8425  cfslb2n  8429  ominf4  8473  fin23lem17  8499  fin23lem28  8501  fin23lem30  8503  fin23lem31  8504  fin23lem40  8512  isfin1-3  8547  dfacfin7  8560  fin1a2lem6  8566  itunitc1  8581  axcc3  8599  dcomex  8608  axdc2lem  8609  axcclem  8618  zfac  8621  ac3  8623  ackm  8626  axac2  8627  axac  8628  axaci  8629  cardeqv  8630  numth2  8632  numth  8633  brdom3  8687  fin71ac  8692  cardf  8706  aleph1  8727  cfpwsdom  8740  smobeth  8742  zfcndrep  8773  zfcndpow  8775  zfcndac  8778  gch2  8834  wunex3  8900  tskpr  8929  inar1  8934  rankcf  8936  tskcard  8940  tskuni  8942  grothpw  8985  axgroth4  8991  grothprim  8993  inaprc  8995  dmaddpi  9051  dmmulpi  9052  1lt2pi  9066  addpqf  9105  mulpqf  9107  1lt2nq  9134  supsrlem  9270  ssxr  9436  gtso  9448  subf  9604  negne0i  9675  negdii  9684  mulnzcnopr  9974  infmsup  10300  halflt1  10535  nn0ssz  10659  zeo  10719  numlt  10766  numltc  10767  uzf  10856  uzinfmi  10926  xaddf  11186  xsubge0  11216  xmulf  11227  infmxrcl  11271  infmxrlb  11288  infmxrgelb  11289  xrinfm0  11291  ixxf  11302  ixxssxr  11304  iooval2  11325  ioof  11379  unirnioo  11381  dfioo2  11382  fzval2  11432  fzf  11433  fz10  11462  fzpreddisj  11496  4fvwrd4  11525  fzof  11542  fzo0  11565  fzo0ss1  11571  injresinjlem  11630  om2uzoi  11770  faclbnd4lem1  12061  hashkf  12097  hashgval  12098  hashinf  12100  hashresfn  12103  hashnn0n0nn  12145  hashge3el3dif  12179  hashbclem  12197  wrdexg  12236  rev0  12396  f1oun2prg  12519  sqr2gt1lt2  12756  limsupgord  12942  limsupval  12944  fclim  13023  fsumrelem  13262  ackbijnn  13283  incexclem  13291  incexc  13292  arisum2  13315  georeclim  13324  geoisumr  13330  0.999...  13333  geoihalfsum  13334  ege2le3  13367  sin0  13425  ef01bndlem  13460  cos2bnd  13464  cos01gt0  13467  sincos2sgn  13470  sin4lt0  13471  rpnnen2lem3  13491  rpnnen2lem9  13497  rexpen  13502  cnso  13521  dvdslelem  13569  n2dvds1  13574  divalglem1  13590  divalglem5  13593  divalglem6  13594  divalglem10  13598  0bits  13627  sadcf  13641  sadcadd  13646  bitsshft  13663  smupf  13666  gcdf  13695  eucalgf  13750  isprm3  13764  2prm  13771  dfphi2  13841  reumodprminv  13864  pockthi  13960  prmreclem2  13970  prmrec  13975  vdwapf  14025  vdwap0  14029  vdwlem6  14039  ramval  14061  ramcl2lem  14062  karatsuba  14105  1259lem5  14151  2503lem3  14155  4001lem4  14160  structcnvcnv  14177  structfn  14179  strlemor1  14257  strleun  14260  prdsval  14385  prdsds  14394  imasdsfn  14444  imasdsval  14445  imasvscafn  14467  xpsc0  14490  xpsc1  14491  xpsff1o  14498  sscpwex  14720  wunfunc  14801  wunnat  14858  eldmcoa  14925  coapm  14931  catcfuccl  14969  catcxpccl  15009  yonedainv  15083  plusffval  15419  grpinvfvi  15570  mulgfvi  15622  symgsssg  15964  symgfisg  15965  psgnunilem5  15991  sylow3lem2  16118  oppglsm  16132  efgmf  16201  efgval  16205  efgsf  16217  0frgp  16267  gsumzaddlem  16399  gsumzaddlemOLD  16401  dmdprd  16470  dprdval  16475  dprdvalOLD  16477  invrfval  16755  drngui  16818  scaffval  16946  lssintcl  17025  mplsubrglem  17497  mplsubrglemOLD  17498  opsrtoslem2  17546  cnfld0  17820  cnfld1  17821  cnfldsub  17824  xrsds  17836  psgnghm  17990  zrhpsgnmhm  17994  psgnodpmr  18000  recrng  18031  ipffval  18057  ocv1  18084  dsmmbas2  18142  frlmip  18183  mdetralt  18394  maducoeval2  18426  eltpsi  18531  fctop  18588  cctop  18590  ppttop  18591  epttop  18593  leordtvallem1  18794  leordtvallem2  18795  iccordt  18798  iscnp2  18823  discmp  18981  concompcld  19018  1stcrestlem  19036  2ndcdisj  19040  topnlly  19075  disllycmp  19082  dis1stc  19083  txuni2  19118  xkotf  19138  dfac14lem  19170  prdstps  19182  txindis  19187  tx1stc  19203  xkohaus  19206  xkoptsub  19207  cnmpt1st  19221  cnmpt2nd  19222  ptcmpfi  19366  filcon  19436  trfil1  19439  fin1aufil  19485  tgpconcompeqg  19662  tgpconcomp  19663  tsmsresOLD  19697  tsmsres  19698  trust  19784  met1stc  20076  dscmet  20145  nmoval  20274  retopon  20322  cnfldtopon  20342  xrsxmet  20366  xrsmopn  20369  metdsval  20403  iimulcn  20490  icopnfhmeo  20495  iccpnfhmeo  20497  xrhmeo  20498  cnheiborlem  20506  lebnumii  20518  ishtpy  20524  htpycc  20532  pco1  20567  pcohtpylem  20571  pcopt  20574  pcopt2  20575  pcoass  20576  pcorevlem  20578  cfilresi  20786  rrxip  20874  rrxcph  20876  ovolval  20937  ovolf  20945  ovoliunlem3  20967  ovolicc1  20979  ovolicc2  20985  volf  20992  ioorf  21033  dyadf  21051  dyadmbl  21060  vitalilem5  21072  vitali  21073  mbfimaopnlem  21113  mbflimsup  21124  0plef  21130  i1fima  21136  i1fima2  21137  i1fd  21139  itg1ge0  21144  itg10  21146  i1f1lem  21147  i1fadd  21153  i1fmul  21154  i1fmulc  21161  mbfi1fseqlem5  21177  itg2addlem  21216  reldv  21325  dvbsss  21357  dvef  21432  lhop1lem  21465  deg1fvi  21536  plypf1  21660  coeeulem  21672  coeeu  21673  vieta1lem2  21757  aannenlem3  21776  aalioulem3  21780  dvradcnv  21866  pserulm  21867  pserdvlem2  21873  abelthlem6  21881  sinhalfpilem  21905  sincos4thpi  21955  tan4thpi  21956  sincos6thpi  21957  pige3  21959  resinf1o  21972  tanord1  21973  tanregt0  21975  relogrn  21993  dfrelog  21997  logneg  22016  logltb  22028  logcn  22072  logf1o2  22075  dvlog  22076  efopnlem2  22082  efopn  22083  logccv  22088  dvsqr  22162  cxpcn3  22166  angpined  22205  1cubr  22217  asinsin  22267  asin1  22269  reasinsin  22271  atan0  22283  atanbnd  22301  atan1  22303  log2cnv  22319  log2ublem3  22323  log2ub  22324  birthday  22328  amgmlem  22363  emcllem5  22373  emgt0  22380  harmonicbnd3  22381  ftalem3  22392  basellem4  22401  sgmf  22463  ppi1  22482  cht1  22483  vma1  22484  ppiltx  22495  sqff1o  22500  ppiublem1  22521  ppiublem2  22522  ppiub  22523  chtub  22531  dchreq  22577  bposlem7  22609  bposlem8  22610  bposlem9  22611  lgsdir2lem2  22643  lgsdir2lem3  22644  chebbnd1  22701  chto1ub  22705  chpo1ubb  22710  pntibndlem1  22818  tgldimor  22935  tglnfn  22961  legov  22996  legtrid  23002  axlowdimlem4  23159  axlowdimlem13  23168  axlowdimlem16  23171  axlowdim1  23173  axlowdim  23175  ecgrtg  23197  umgrafi  23224  usgraexmpl  23287  usgrafilem1  23292  2trllemA  23417  wlkntrllem1  23426  wlkntrllem3  23428  0pth  23437  spthispth  23440  2pthon  23469  2pthon3v  23471  redwlk  23473  constr3trllem3  23506  constr3pthlem3  23511  konigsberg  23576  ex-dif  23598  ex-un  23599  ex-in  23600  ex-fl  23622  avril1  23624  ginvsn  23804  cnid  23806  mulid  23811  rngosn3  23881  vcoprnelem  23924  vcoprne  23925  vcex  23926  cnnvm  24041  ipasslem8  24205  ipasslem10  24207  hvsubf  24385  normlem1  24480  normlem6  24485  normlem7  24486  norm-ii-i  24507  norm3adifii  24518  hilid  24531  hlimf  24608  norm1exi  24621  hhssabloi  24631  hhssnv  24633  hhshsslem1  24636  shincli  24733  shsval2i  24758  shs0i  24820  chj0i  24826  chm1i  24827  chincli  24831  chdmm1i  24848  shjshsi  24863  chsup0  24919  h1de2bi  24925  spansnpji  24949  cmcmlem  24962  cmcmii  24968  cmcm2ii  24969  cmcm3ii  24970  pjidmi  25044  pjssmii  25052  pj0i  25064  pjocini  25069  mayetes3i  25101  df0op2  25124  hoaddcomi  25144  hoaddassi  25148  hocadddiri  25151  hocsubdiri  25152  hoaddid1i  25158  ho0coi  25160  hoid1i  25161  hoid1ri  25162  hodseqi  25166  honegsubi  25168  adj1o  25266  hoddii  25361  lnopunilem1  25382  lnopunilem2  25383  nmcopexi  25399  nmcopex  25401  nmcoplb  25402  nmcfnexi  25423  nmcfnex  25425  nmcfnlb  25426  adjbd1o  25457  adjcoi  25472  nmopcoadji  25473  opsqrlem6  25517  pjsdii  25527  pjddii  25528  pjidmcoi  25549  pjtoi  25551  pjin1i  25564  pjclem1  25567  stji1i  25614  largei  25639  spc2ed  25825  reuxfr3d  25841  inindif  25865  iuninc  25879  fnresin  25915  rinvf1o  25917  suppss2f  25922  xppreima  25932  ofoprabco  25950  funcnvmptOLD  25954  gtiso  25964  df1stres  25967  df2ndres  25968  snct  25979  dmct  25982  ffsrn  25997  resf1o  25998  fpwrelmapffs  26002  xrge0infssd  26022  nnindf  26057  nn0min  26058  ressplusf  26079  xrsclat  26109  xrge0base  26114  xrge00  26115  xrge0neqmnf  26120  xrnarchi  26169  orngsqr  26240  xrge0slmod  26281  unicls  26302  sqsscirc1  26307  ordtconlem1  26323  mhmhmeotmd  26326  rmulccn  26327  raddcn  26328  xrge0iifiso  26334  xrge0iifhmeo  26335  lmxrge0  26351  cnzh  26368  rezh  26369  qqh0  26382  qqh1  26383  qqhre  26415  rrhre  26416  rnlogblem  26427  log2le1  26435  ind1a  26446  esumnul  26471  esum0  26472  esumsn  26484  esumpfinvallem  26492  esumpfinvalf  26494  esumpcvgval  26496  sigaclfu2  26533  dmsigagen  26556  ddemeas  26621  imambfm  26646  mbfmvolf  26650  br2base  26653  omsfval  26678  oms0  26679  sibfof  26695  sitg0  26701  eulerpartlemt  26723  eulerpartgbij  26724  fib5  26757  probdif  26772  0rrv  26803  coinfliplem  26830  coinflipprob  26831  coinfliprv  26834  ballotlem2  26840  ballotlem4  26850  ballotlem5  26851  ballotlemi  26852  ballotlemiex  26853  ballotlemi1  26854  ballotlemii  26855  ballotlemsup  26856  ballotlemimin  26857  ballotlemfrcn0  26881  ballotlemirc  26883  ballotlem7  26887  ballotth  26889  signsplypnf  26920  signsply0  26921  signsw0g  26926  signswch  26931  signsvvf  26949  signsvf0  26950  subfacf  27032  subfacp1lem1  27036  subfacp1lem5  27041  subfacp1lem6  27042  subfacval3  27046  erdszelem2  27049  erdszelem9  27056  erdszelem11  27058  kur14lem4  27066  iooscon  27105  iccllyscon  27108  problem5  27271  quad3  27272  ghomgrpilem1  27273  ghomgrpilem2  27274  circum  27288  axextprim  27321  axrepprim  27322  axunprim  27323  axinfprim  27326  axacprim  27327  inffz  27356  risefall0lem  27498  setinds  27560  dfon2lem2  27566  dfon2lem4  27568  dfrdg2  27578  axextdfeq  27580  poseq  27683  wfrlem4  27696  frrlem4  27740  sltval2  27766  nosgnn0  27768  sltintdifex  27773  sltres  27774  sltsolem1  27778  bdayfo  27785  symdifV  27825  fobigcup  27900  snelsingles  27922  fullfunfnv  27946  fullfunfv  27947  dfrdg4  27950  rankaltopb  27979  linedegen  28143  rank0  28177  rankeq1o  28178  hfuni  28191  nabi1i  28207  nabi2i  28208  limsucncmpi  28261  tan2h  28395  heicant  28397  mblfinlem1  28399  mblfinlem2  28400  ovoliunnfl  28404  voliunnfl  28406  dvtanlem  28412  itg2addnclem  28414  itg2addnclem2  28415  dvcnsqr  28449  asindmre  28450  areacirclem1  28455  gtinf  28485  fneer  28531  neibastop1  28551  opelopab3  28581  fdc  28612  cntotbnd  28666  heiborlem6  28686  rrnval  28697  reheibor  28709  impor  28852  prter2  28997  diophrw  29068  0dioph  29088  rabren3dioph  29125  rencldnfilem  29130  pellexlem6  29146  pellex  29147  pellfundval  29192  frmx  29225  frmy  29226  jm2.23  29316  jm2.27dlem3  29331  axac10  29353  pw2f1ocnv  29357  wepwsolem  29365  kelac2lem  29388  lmhmlnmsplit  29411  pwfi2f1o  29422  frlmpwfi  29424  dgraaval  29472  dgraaf  29475  seff  29566  expgrowthi  29578  expgrowth  29580  refsum2cnlem1  29730  infrglb  29742  dvcosre  29759  stoweidlem1  29767  stoweidlem26  29792  stoweidlem34  29800  stoweidlem44  29810  stoweid  29829  stirlinglem5  29844  axorbtnotaiffb  29888  axorbciffatcxorb  29890  abnotbtaxb  29901  resisresindm  30110  wwlktovf  30222  frgrawopreg2  30615  ldepslinc  30982  comraddi  31045  alimp-no-surprise  31062  ee233  31153  ax6e2nd  31196  in1  31213  dfvd2ani  31225  dfvd2i  31227  dfvd3i  31234  dfvd3ani  31237  e0bi  31438  uun2221  31475  uun2221p1  31476  uun2221p2  31477  en3lpVD  31510  relopabVD  31566  ax6e2ndVD  31573  ax6e2ndALT  31595  bnj521  31657  bnj1098  31706  bnj1109  31709  bnj1131  31710  bnj1533  31774  bnj151  31799  bnj580  31835  bnj852  31843  bnj864  31844  bnj865  31845  bnj978  31871  bnj1021  31886  bnj907  31887  bnj1093  31900  bnj1145  31913  bnj1172  31921  bnj1174  31923  bnj1176  31925  bnj1186  31927  bj-nfxfr  32081  bj-axsep  32215  bj-zfpow  32217  bj-dtru  32219  bj-n0i  32338  bj-snsetex  32356  bj-tagss  32373  bj-2upln0  32416  bj-2upln1upl  32417  bj-pinftyccb  32444  bj-minftyccb  32448  bj-pinftynminfty  32450  renegclALT  32507  mapdunirnN  35188
  Copyright terms: Public domain W3C validator