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  880  pm5.16  888  biluk  931  4exmid  937  dn1  964  3ori  1288  trubifal  1418  cadan  1443  nic-dfim  1486  nic-dfneg  1487  nic-mp  1488  nic-mpALT  1489  tbw-negdf  1516  rb-imdf  1567  mpgbi  1604  19.35i  1666  19.36i  1914  19.36aiv  1936  19.37aiv  1944  ax6  1972  sbie  2123  sbieOLD  2124  sbcoOLD  2130  sbidmOLD  2133  axi12  2443  bm1.1  2450  eqcomi  2480  eqtri  2496  eleqtri  2553  neii  2666  necomi  2737  nesymiOLD  2741  neeqtri  2765  neli  2802  nrex  2919  rexlimi  2945  rexlimiv  2949  isseti  3119  vtocl2  3166  vtocl3  3167  eueq1  3276  euxfr2  3288  cdeqri  3317  sseqtri  3536  3sstr3i  3542  pssn2lp  3605  equncomi  3650  unssi  3679  ssini  3721  unabs  3728  inabs  3729  dfin4  3738  npss0  3865  difid  3895  disjdif  3899  difin0  3900  snid  4055  iinrab2  4388  rintn0  4416  breqtri  4470  axsep  4567  bm1.3ii  4571  ax6vsep  4572  zfnuleu  4573  notzfaus  4622  zfpow  4626  dtru  4638  reusv2lem4  4651  reuxfr2d  4670  dtruALT  4679  dtruALT2  4691  op1stb  4717  copsexg  4732  copsexgOLD  4733  uniop  4750  pwundif  4787  onunisuci  4991  relop  5151  rn0  5252  dmresi  5327  issref  5378  somincom  5402  cnvcnv  5457  rescnvcnv  5468  cnvcnvres  5469  cnvsn  5489  cocnvcnv2  5517  cores2  5518  co01  5520  relcoi1  5534  cnviin  5542  iota4an  5568  fnopab  5703  mpt0  5706  fnmpti  5707  f1cnvcnv  5787  f1ovi  5850  eliman0  5893  fvco4i  5943  fmpti  6042  fvsnun2  6095  funiunfv  6146  oprabss  6370  relmptopab  6505  zfun  6575  tfinds2  6676  omon  6689  2nd0  6788  f1stres  6803  f2ndres  6804  relmpt2opab  6862  df1st2  6866  df2nd2  6867  fsplit  6885  reldmtpos  6960  dftpos4  6971  tpostpos  6972  tpos0  6982  smo0  7026  tfrlem14  7057  tfrlem16  7059  rdgsucg  7086  rdglimg  7088  frfnom  7097  oawordeulem  7200  uniixp  7489  dfdom2  7538  ssdomg  7558  xpcomf1o  7603  sbthlem5  7628  pwdom  7666  limensuci  7690  fiint  7793  fidomdm  7798  pwfilem  7810  mptfi  7815  fisn  7883  dffi3  7887  ordtypelem6  7944  ordtypelem7  7945  wemaplem2  7968  wdompwdom  8000  harwdom  8012  suc11reg  8032  zfinf  8052  axinf2  8053  noinfep  8072  cantnfvalf  8080  cantnflt  8087  cantnf0  8090  cantnf  8108  cantnfltOLD  8117  cantnfOLD  8130  tz9.1c  8157  tc2  8169  r111  8189  r1tr2  8191  r1ordg  8192  r1sssuc  8197  r1val1  8200  tz9.13  8205  r1elssi  8219  pwwf  8221  rankopb  8266  rankeq0b  8274  ranksuc  8279  rankmapu  8292  rankxplim  8293  rankxplim3  8295  rankxpsuc  8296  cp  8305  karden  8309  card0  8335  cardlim  8349  cardom  8363  infxpenlem  8387  alephsuc2  8457  alephgeom  8459  unialeph  8478  dfac4  8499  dfacacn  8517  cda1dif  8552  pm110.643  8553  infcda1  8569  ackbij1lem13  8608  ackbij2  8619  cf0  8627  cfsuc  8633  cfom  8640  cfslb2n  8644  ominf4  8688  fin23lem17  8714  fin23lem28  8716  fin23lem30  8718  fin23lem31  8719  fin23lem40  8727  isfin1-3  8762  dfacfin7  8775  fin1a2lem6  8781  itunitc1  8796  axcc3  8814  dcomex  8823  axdc2lem  8824  axcclem  8833  zfac  8836  ac3  8838  ackm  8841  axac2  8842  axac  8843  axaci  8844  cardeqv  8845  numth2  8847  numth  8848  brdom3  8902  fin71ac  8907  cardf  8921  aleph1  8942  cfpwsdom  8955  smobeth  8957  zfcndrep  8988  zfcndpow  8990  zfcndac  8993  gch2  9049  wunex3  9115  tskpr  9144  inar1  9149  rankcf  9151  tskcard  9155  tskuni  9157  grothpw  9200  axgroth4  9206  grothprim  9208  inaprc  9210  dmaddpi  9264  dmmulpi  9265  1lt2pi  9279  addpqf  9318  mulpqf  9320  1lt2nq  9347  supsrlem  9484  ssxr  9650  gtso  9662  subf  9818  negne0i  9890  negdii  9899  mulnzcnopr  10191  infmsup  10517  halflt1  10753  nn0ssz  10881  zeo  10942  numlt  10991  numltc  10992  uzf  11081  uzinfmi  11157  xaddf  11419  xsubge0  11449  xmulf  11460  infmxrcl  11504  infmxrlb  11521  infmxrgelb  11522  xrinfm0  11524  ixxf  11535  ixxssxr  11537  iooval2  11558  ioof  11618  unirnioo  11620  dfioo2  11621  fzval2  11671  fzf  11672  fz10  11702  fzpreddisj  11725  4fvwrd4  11786  fzof  11790  fzo0  11813  fzo0ss1  11819  injresinjlem  11889  om2uzoi  12030  faclbnd4lem1  12335  hashkf  12371  hashgval  12372  hashinf  12374  hashresfn  12377  hashnn0n0nn  12422  hashbclem  12463  hashge3el3dif  12486  wrdexg  12519  rev0  12697  f1oun2prg  12824  wwlktovf  12853  sqrt2gt1lt2  13067  limsupgord  13254  limsupval  13256  fclim  13335  fsumrelem  13580  ackbijnn  13599  incexclem  13607  incexc  13608  arisum2  13631  georeclim  13640  geoisumr  13646  0.999...  13649  geoihalfsum  13650  ege2le3  13683  sin0  13741  ef01bndlem  13776  cos2bnd  13780  cos01gt0  13783  sincos2sgn  13786  sin4lt0  13787  rpnnen2lem3  13807  rpnnen2lem9  13813  rexpen  13818  cnso  13837  dvdslelem  13885  n2dvds1  13890  divalglem1  13907  divalglem5  13910  divalglem6  13911  divalglem10  13915  0bits  13944  sadcf  13958  sadcadd  13963  bitsshft  13980  smupf  13983  gcdf  14012  eucalgf  14067  isprm3  14081  2prm  14088  dfphi2  14159  reumodprminv  14184  pockthi  14280  prmreclem2  14290  prmrec  14295  vdwapf  14345  vdwap0  14349  vdwlem6  14359  ramval  14381  ramcl2lem  14382  karatsuba  14425  1259lem5  14471  2503lem3  14475  4001lem4  14480  structcnvcnv  14497  structfn  14499  strlemor1  14578  strleun  14581  prdsval  14706  prdsds  14715  imasdsfn  14765  imasdsval  14766  imasvscafn  14788  xpsc0  14811  xpsc1  14812  xpsff1o  14819  sscpwex  15041  wunfunc  15122  wunnat  15179  eldmcoa  15246  coapm  15252  catcfuccl  15290  catcxpccl  15330  yonedainv  15404  plusffval  15740  grpinvfvi  15892  mulgfvi  15946  symgsssg  16288  symgfisg  16289  psgnunilem5  16315  sylow3lem2  16444  oppglsm  16458  efgmf  16527  efgval  16531  efgsf  16543  0frgp  16593  gsumzaddlem  16725  gsumzaddlemOLD  16727  dmdprd  16820  dprdval  16825  dprdvalOLD  16827  invrfval  17106  drngui  17185  scaffval  17313  lssintcl  17393  mplsubrglem  17871  mplsubrglemOLD  17872  opsrtoslem2  17920  cnfld0  18213  cnfld1  18214  cnfldsub  18217  xrsds  18229  psgnghm  18383  zrhpsgnmhm  18387  psgnodpmr  18393  recrng  18424  ipffval  18450  ocv1  18477  dsmmbas2  18535  frlmip  18576  mdetralt  18877  maducoeval2  18909  fvmptnn04if  19117  eltpsi  19214  fctop  19271  cctop  19273  ppttop  19274  epttop  19276  leordtvallem1  19477  leordtvallem2  19478  iccordt  19481  iscnp2  19506  discmp  19664  concompcld  19701  1stcrestlem  19719  2ndcdisj  19723  topnlly  19758  disllycmp  19765  dis1stc  19766  txuni2  19801  xkotf  19821  dfac14lem  19853  prdstps  19865  txindis  19870  tx1stc  19886  xkohaus  19889  xkoptsub  19890  cnmpt1st  19904  cnmpt2nd  19905  ptcmpfi  20049  filcon  20119  trfil1  20122  fin1aufil  20168  tgpconcompeqg  20345  tgpconcomp  20346  tsmsresOLD  20380  tsmsres  20381  trust  20467  met1stc  20759  dscmet  20828  nmoval  20957  retopon  21005  cnfldtopon  21025  xrsxmet  21049  xrsmopn  21052  metdsval  21086  iimulcn  21173  icopnfhmeo  21178  iccpnfhmeo  21180  xrhmeo  21181  cnheiborlem  21189  lebnumii  21201  ishtpy  21207  htpycc  21215  pco1  21250  pcohtpylem  21254  pcopt  21257  pcopt2  21258  pcoass  21259  pcorevlem  21261  cfilresi  21469  rrxip  21557  rrxcph  21559  ovolval  21620  ovolf  21628  ovoliunlem3  21650  ovolicc1  21662  ovolicc2  21668  volf  21675  ioorf  21717  dyadf  21735  dyadmbl  21744  vitalilem5  21756  vitali  21757  mbfimaopnlem  21797  mbflimsup  21808  0plef  21814  i1fima  21820  i1fima2  21821  i1fd  21823  itg1ge0  21828  itg10  21830  i1f1lem  21831  i1fadd  21837  i1fmul  21838  i1fmulc  21845  mbfi1fseqlem5  21861  itg2addlem  21900  reldv  22009  dvbsss  22041  dvef  22116  lhop1lem  22149  deg1fvi  22220  plypf1  22344  coeeulem  22356  coeeu  22357  vieta1lem2  22441  aannenlem3  22460  aalioulem3  22464  dvradcnv  22550  pserulm  22551  pserdvlem2  22557  abelthlem6  22565  sinhalfpilem  22589  sincos4thpi  22639  tan4thpi  22640  sincos6thpi  22641  pige3  22643  resinf1o  22656  tanord1  22657  tanregt0  22659  relogrn  22677  dfrelog  22681  logneg  22700  logltb  22712  logcn  22756  logf1o2  22759  dvlog  22760  efopnlem2  22766  efopn  22767  logccv  22772  dvsqrt  22846  cxpcn3  22850  angpined  22889  1cubr  22901  asinsin  22951  asin1  22953  reasinsin  22955  atan0  22967  atanbnd  22985  atan1  22987  log2cnv  23003  log2ublem3  23007  log2ub  23008  birthday  23012  amgmlem  23047  emcllem5  23057  emgt0  23064  harmonicbnd3  23065  ftalem3  23076  basellem4  23085  sgmf  23147  ppi1  23166  cht1  23167  vma1  23168  ppiltx  23179  sqff1o  23184  ppiublem1  23205  ppiublem2  23206  ppiub  23207  chtub  23215  dchreq  23261  bposlem7  23293  bposlem8  23294  bposlem9  23295  lgsdir2lem2  23327  lgsdir2lem3  23328  chebbnd1  23385  chto1ub  23389  chpo1ubb  23394  pntibndlem1  23502  tgldimor  23621  tglnfn  23662  legov  23699  legtrid  23705  axlowdimlem4  23924  axlowdimlem13  23933  axlowdimlem16  23936  axlowdim1  23938  axlowdim  23940  ecgrtg  23962  umgrafi  23998  usgraexmpl  24077  usgraexmplc  24080  usgrafilem1  24087  2trllemA  24228  wlkntrllem1  24237  wlkntrllem3  24239  0pth  24248  spthispth  24251  2pthon  24280  2pthon3v  24282  constr3trllem3  24328  constr3pthlem3  24333  konigsberg  24663  frgrawopreg2  24728  ex-dif  24821  ex-un  24822  ex-in  24823  ex-fl  24845  avril1  24847  ginvsn  25027  cnid  25029  mulid  25034  rngosn3  25104  vcoprnelem  25147  vcoprne  25148  vcex  25149  cnnvm  25264  ipasslem8  25428  ipasslem10  25430  hvsubf  25608  normlem1  25703  normlem6  25708  normlem7  25709  norm-ii-i  25730  norm3adifii  25741  hilid  25754  hlimf  25831  norm1exi  25844  hhssabloi  25854  hhssnv  25856  hhshsslem1  25859  shincli  25956  shsval2i  25981  shs0i  26043  chj0i  26049  chm1i  26050  chincli  26054  chdmm1i  26071  shjshsi  26086  chsup0  26142  h1de2bi  26148  spansnpji  26172  cmcmlem  26185  cmcmii  26191  cmcm2ii  26192  cmcm3ii  26193  pjidmi  26267  pjssmii  26275  pj0i  26287  pjocini  26292  mayetes3i  26324  df0op2  26347  hoaddcomi  26367  hoaddassi  26371  hocadddiri  26374  hocsubdiri  26375  hoaddid1i  26381  ho0coi  26383  hoid1i  26384  hoid1ri  26385  hodseqi  26389  honegsubi  26391  adj1o  26489  hoddii  26584  lnopunilem1  26605  lnopunilem2  26606  nmcopexi  26622  nmcopex  26624  nmcoplb  26625  nmcfnexi  26646  nmcfnex  26648  nmcfnlb  26649  adjbd1o  26680  adjcoi  26695  nmopcoadji  26696  opsqrlem6  26740  pjsdii  26750  pjddii  26751  pjidmcoi  26772  pjtoi  26774  pjin1i  26787  pjclem1  26790  stji1i  26837  largei  26862  spc2ed  27048  reuxfr3d  27064  inindif  27088  iuninc  27101  fnresin  27143  rinvf1o  27145  suppss2f  27150  xppreima  27159  ofoprabco  27177  funcnvmptOLD  27181  gtiso  27191  df1stres  27194  df2ndres  27195  snct  27206  dmct  27209  ffsrn  27224  resf1o  27225  fpwrelmapffs  27229  xrge0infssd  27249  nnindf  27278  nn0min  27279  ressplusf  27300  xrsclat  27330  xrge0base  27335  xrge00  27336  xrge0neqmnf  27341  xrnarchi  27390  orngsqr  27457  xrge0slmod  27497  unicls  27521  sqsscirc1  27526  ordtconlem1  27542  mhmhmeotmd  27545  rmulccn  27546  raddcn  27547  xrge0iifiso  27553  xrge0iifhmeo  27554  lmxrge0  27570  cnzh  27587  rezh  27588  qqh0  27601  qqh1  27602  qqhre  27634  rrhre  27635  rnlogblem  27655  log2le1  27663  ind1a  27674  esumnul  27699  esum0  27700  esumsn  27712  esumpfinvallem  27720  esumpfinvalf  27722  esumpcvgval  27724  sigaclfu2  27761  dmsigagen  27784  ddemeas  27848  imambfm  27873  mbfmvolf  27877  br2base  27880  omsfval  27905  oms0  27906  sibfof  27922  sitg0  27928  eulerpartlemt  27950  eulerpartgbij  27951  fib5  27984  probdif  27999  0rrv  28030  coinfliplem  28057  coinflipprob  28058  coinfliprv  28061  ballotlem2  28067  ballotlem4  28077  ballotlem5  28078  ballotlemi  28079  ballotlemiex  28080  ballotlemi1  28081  ballotlemii  28082  ballotlemsup  28083  ballotlemimin  28084  ballotlemfrcn0  28108  ballotlemirc  28110  ballotlem7  28114  ballotth  28116  signsplypnf  28147  signsply0  28148  signsw0g  28153  signswch  28158  signsvvf  28176  signsvf0  28177  subfacf  28259  subfacp1lem1  28263  subfacp1lem5  28268  subfacp1lem6  28269  subfacval3  28273  erdszelem2  28276  erdszelem9  28283  erdszelem11  28285  kur14lem4  28293  iooscon  28332  iccllyscon  28335  problem5  28498  quad3  28499  ghomgrpilem1  28500  ghomgrpilem2  28501  circum  28515  axextprim  28548  axrepprim  28549  axunprim  28550  axinfprim  28553  axacprim  28554  inffz  28583  risefall0lem  28725  setinds  28787  dfon2lem2  28793  dfon2lem4  28795  dfrdg2  28805  axextdfeq  28807  poseq  28910  wfrlem4  28923  frrlem4  28967  sltval2  28993  nosgnn0  28995  sltintdifex  29000  sltres  29001  sltsolem1  29005  bdayfo  29012  symdifV  29052  fobigcup  29127  snelsingles  29149  fullfunfnv  29173  fullfunfv  29174  dfrdg4  29177  rankaltopb  29206  linedegen  29370  rank0  29404  rankeq1o  29405  hfuni  29418  nabi1i  29434  nabi2i  29435  limsucncmpi  29487  tan2h  29624  heicant  29626  mblfinlem1  29628  mblfinlem2  29629  ovoliunnfl  29633  voliunnfl  29635  dvtanlem  29641  itg2addnclem  29643  itg2addnclem2  29644  dvcnsqrt  29678  asindmre  29679  areacirclem1  29684  gtinf  29714  fneer  29760  neibastop1  29780  opelopab3  29810  fdc  29841  cntotbnd  29895  heiborlem6  29915  rrnval  29926  reheibor  29938  impor  30081  prter2  30226  diophrw  30296  0dioph  30316  rabren3dioph  30353  rencldnfilem  30358  pellexlem6  30374  pellex  30375  pellfundval  30420  frmx  30453  frmy  30454  jm2.23  30542  jm2.27dlem3  30557  axac10  30579  pw2f1ocnv  30583  wepwsolem  30591  kelac2lem  30614  lmhmlnmsplit  30637  pwfi2f1o  30648  frlmpwfi  30650  dgraaval  30698  dgraaf  30701  seff  30792  expgrowthi  30838  expgrowth  30840  refsum2cnlem1  30990  negpilt0  31039  ssfiunibd  31086  ioontr  31113  iccdifioo  31119  iccdifprioo  31120  infrglb  31140  islptre  31161  sumnnodd  31172  icccncfext  31226  cncfiooicclem1  31232  dvcosre  31239  dvsinax  31241  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  volioc  31290  iblcncfioo  31296  stoweidlem1  31301  stoweidlem26  31326  stoweidlem34  31334  stoweidlem44  31344  stoweid  31363  stirlinglem5  31378  dirkertrigeqlem3  31400  dirkercncflem1  31403  dirkercncflem2  31404  fourierdlem20  31427  fourierdlem26  31433  fourierdlem32  31439  fourierdlem43  31450  fourierdlem44  31451  fourierdlem49  31456  fourierdlem56  31463  fourierdlem62  31469  fourierdlem63  31470  fourierdlem65  31472  fourierdlem74  31481  fourierdlem75  31482  fourierdlem81  31488  fourierdlem82  31489  fourierdlem83  31490  fourierdlem89  31496  fourierdlem91  31498  fourierdlem100  31507  fourierdlem102  31509  fourierdlem103  31510  fourierdlem104  31511  fourierdlem108  31515  fourierdlem111  31518  fourierdlem112  31519  fourierdlem114  31521  fourierswlem  31531  fouriersw  31532  axorbtnotaiffb  31565  axorbciffatcxorb  31567  abnotbtaxb  31578  resisresindm  31774  residfi  31783  ldepslinc  32191  comraddi  32258  alimp-no-surprise  32277  ee233  32368  ax6e2nd  32411  in1  32428  dfvd2ani  32440  dfvd2i  32442  dfvd3i  32449  dfvd3ani  32452  e0bi  32653  uun2221  32690  uun2221p1  32691  uun2221p2  32692  en3lpVD  32725  relopabVD  32781  ax6e2ndVD  32788  ax6e2ndALT  32810  bnj521  32872  bnj1098  32921  bnj1109  32924  bnj1131  32925  bnj1533  32989  bnj151  33014  bnj580  33050  bnj852  33058  bnj864  33059  bnj865  33060  bnj978  33086  bnj1021  33101  bnj907  33102  bnj1093  33115  bnj1145  33128  bnj1172  33136  bnj1174  33138  bnj1176  33140  bnj1186  33142  bj-nfxfr  33306  bj-axsep  33460  bj-zfpow  33462  bj-dtru  33464  bj-n0i  33584  bj-snsetex  33602  bj-tagss  33619  bj-2upln0  33662  bj-2upln1upl  33663  bj-nuliota  33667  bj-elid  33672  bj-pinftyccb  33696  bj-minftyccb  33700  bj-pinftynminfty  33702  renegclALT  33766  mapdunirnN  36447  trclubg  36795
  Copyright terms: Public domain W3C validator