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  294  pm5.19  358  ori  373  imori  411  pm4.71i  630  pm4.71ri  631  pm5.32i  635  pm3.24  880  pm5.16  888  biluk  931  4exmid  937  dn1  964  3ori  1286  trubifal  1437  cadan  1462  nic-dfim  1506  nic-dfneg  1507  nic-mp  1508  nic-mpALT  1509  tbw-negdf  1536  rb-imdf  1587  mpgbi  1626  19.35i  1694  19.36iv  1768  19.37iv  1774  19.36i  1970  ax6  2008  sbie  2151  sbieOLD  2152  sbidmOLD  2159  axi12  2430  bm1.1  2437  eqcomi  2467  eqtri  2483  eleqtri  2540  neii  2653  necomi  2724  nesymiOLD  2728  neeqtri  2752  neli  2789  nrex  2909  rexlimi  2936  rexlimiv  2940  isseti  3112  vtocl2  3159  vtocl3  3160  eueq1  3269  euxfr2  3281  cdeqri  3310  sseqtri  3521  3sstr3i  3527  pssn2lp  3591  equncomi  3636  unssi  3665  ssini  3707  unabs  3725  inabs  3726  dfin4  3735  npss0  3853  difid  3884  disjdif  3888  difin0  3889  snid  4044  iinrab2  4378  symdifv  4393  rintn0  4409  breqtri  4462  axsep  4559  bm1.3ii  4563  ax6vsep  4564  zfnuleu  4565  notzfaus  4612  zfpow  4616  dtru  4628  reusv2lem4  4641  reuxfr2d  4660  dtruALT  4669  dtruALT2  4681  op1stb  4707  copsexg  4722  uniop  4739  pwundif  4776  onunisuci  4980  relop  5142  rn0  5243  dmresi  5317  issref  5368  somincom  5389  cnvcnv  5443  rescnvcnv  5453  cnvcnvres  5454  cnvsn  5474  cocnvcnv2  5502  cores2  5503  co01  5505  relcoi1  5519  cnviin  5527  iota4an  5553  fnopab  5687  mpt0  5690  fnmpti  5691  f1cnvcnv  5771  f1ovi  5834  eliman0  5877  fvco4i  5926  fmpti  6030  fvsnun2  6083  funiunfv  6135  oprabss  6361  relmptopab  6496  zfun  6566  tfinds2  6671  omon  6684  2nd0  6780  f1stres  6795  f2ndres  6796  relmpt2opab  6855  df1st2  6859  df2nd2  6860  fsplit  6878  reldmtpos  6955  dftpos4  6966  tpostpos  6967  tpos0  6977  smo0  7021  tfrlem14  7052  tfrlem16  7054  rdgsucg  7081  rdglimg  7083  frfnom  7092  oawordeulem  7195  uniixp  7485  dfdom2  7534  ssdomg  7554  xpcomf1o  7599  sbthlem5  7624  pwdom  7662  limensuci  7686  fiint  7789  fidomdm  7794  pwfilem  7806  mptfi  7811  fisn  7879  dffi3  7883  ordtypelem6  7940  ordtypelem7  7941  wemaplem2  7964  wdompwdom  7996  harwdom  8008  suc11reg  8027  zfinf  8047  axinf2  8048  noinfep  8067  cantnfvalf  8075  cantnflt  8082  cantnf0  8085  cantnf  8103  cantnfltOLD  8112  cantnfOLD  8125  tz9.1c  8152  tc2  8164  r111  8184  r1tr2  8186  r1ordg  8187  r1sssuc  8192  r1val1  8195  tz9.13  8200  r1elssi  8214  pwwf  8216  rankopb  8261  rankeq0b  8269  ranksuc  8274  rankmapu  8287  rankxplim  8288  rankxplim3  8290  rankxpsuc  8291  cp  8300  karden  8304  card0  8330  cardlim  8344  cardom  8358  infxpenlem  8382  alephsuc2  8452  alephgeom  8454  unialeph  8473  dfac4  8494  dfacacn  8512  cda1dif  8547  pm110.643  8548  infcda1  8564  ackbij1lem13  8603  ackbij2  8614  cf0  8622  cfsuc  8628  cfom  8635  cfslb2n  8639  ominf4  8683  fin23lem17  8709  fin23lem28  8711  fin23lem30  8713  fin23lem31  8714  fin23lem40  8722  isfin1-3  8757  dfacfin7  8770  fin1a2lem6  8776  itunitc1  8791  axcc3  8809  dcomex  8818  axdc2lem  8819  axcclem  8828  zfac  8831  ac3  8833  ackm  8836  axac2  8837  axac  8838  axaci  8839  cardeqv  8840  numth2  8842  numth  8843  brdom3  8897  fin71ac  8902  cardf  8916  aleph1  8937  cfpwsdom  8950  smobeth  8952  zfcndrep  8981  zfcndpow  8983  zfcndac  8986  gch2  9042  wunex3  9108  tskpr  9137  inar1  9142  rankcf  9144  tskcard  9148  tskuni  9150  grothpw  9193  axgroth4  9199  grothprim  9201  inaprc  9203  dmaddpi  9257  dmmulpi  9258  1lt2pi  9272  addpqf  9311  mulpqf  9313  1lt2nq  9340  supsrlem  9477  ssxr  9643  gtso  9655  subf  9813  negne0i  9885  negdiiOLD  9895  mulnzcnopr  10191  infmsup  10516  halflt1  10753  nn0ssz  10881  zeo  10944  numlt  10995  numltc  10996  uzf  11085  uzinfmi  11162  zgt1rpn0n1  11258  xaddf  11426  xsubge0  11456  xmulf  11467  infmxrcl  11511  infmxrlb  11528  infmxrgelb  11529  xrinfm0  11531  ixxf  11542  ixxssxr  11544  iooval2  11565  ioof  11625  unirnioo  11627  dfioo2  11628  fzval2  11678  fzf  11679  fz10  11709  fzpreddisj  11733  4fvwrd4  11797  fzof  11801  fzo0  11826  om2uzoi  12048  faclbnd4lem1  12353  hashkf  12389  hashgval  12390  hashinf  12392  hashresfn  12395  hashnn0n0nn  12442  hashbclem  12485  hashge3el3dif  12508  wrdexg  12544  rev0  12729  f1oun2prg  12856  trclublem  12913  sqrt2gt1lt2  13190  limsupgord  13377  limsupval  13379  fclim  13458  fsumrelem  13703  ackbijnn  13722  incexclem  13730  incexc  13731  arisum2  13754  georeclim  13763  geoisumr  13769  0.999...  13772  geoihalfsum  13773  ege2le3  13907  sin0  13966  ef01bndlem  14001  cos2bnd  14005  cos01gt0  14008  sincos2sgn  14011  sin4lt0  14012  rpnnen2lem3  14034  rpnnen2lem9  14040  rexpen  14045  cnso  14064  dvdslelem  14114  n2dvds1  14119  divalglem1  14136  divalglem5  14139  divalglem6  14140  divalglem10  14144  0bits  14173  sadcf  14187  sadcadd  14192  bitsshft  14209  smupf  14212  gcdf  14241  eucalgf  14296  2prm  14317  dfphi2  14388  pockthi  14509  prmreclem2  14519  prmrec  14524  vdwapf  14574  vdwap0  14578  vdwlem6  14588  ramval  14610  ramcl2lem  14611  karatsuba  14654  1259lem5  14701  2503lem3  14705  4001lem4  14710  structcnvcnv  14727  structfn  14729  strlemor1  14811  strleun  14814  prdsval  14944  prdsds  14953  imasdsfn  15003  imasdsval  15004  imasvscafn  15026  xpsc0  15049  xpsc1  15050  xpsff1o  15057  sscpwex  15303  wunfunc  15387  wunnat  15444  eldmcoa  15543  coapm  15549  catcfuccl  15587  catcxpccl  15675  yonedainv  15749  plusffval  16076  grpinvfvi  16290  mulgfvi  16345  symgsssg  16691  symgfisg  16692  psgnunilem5  16718  sylow3lem2  16847  oppglsm  16861  efgmf  16930  efgval  16934  efgsf  16946  0frgp  16996  gsumzaddlem  17133  gsumzaddlemOLD  17135  dmdprd  17224  dprdval  17229  dprdvalOLD  17231  invrfval  17517  drngui  17597  scaffval  17725  lssintcl  17805  mplsubrglem  18295  mplsubrglemOLD  18296  opsrtoslem2  18344  cnfld0  18637  cnfld1  18638  cnfldsub  18641  xrsds  18656  psgnghm  18789  zrhpsgnmhm  18793  recrng  18830  ipffval  18856  ocv1  18883  dsmmbas2  18941  mdetralt  19277  maducoeval2  19309  eltpsi  19614  unitg  19635  fctop  19672  cctop  19674  ppttop  19675  epttop  19677  leordtvallem1  19878  leordtvallem2  19879  iccordt  19882  iscnp2  19907  discmp  20065  concompcld  20101  1stcrestlem  20119  2ndcdisj  20123  topnlly  20158  disllycmp  20165  dis1stc  20166  txuni2  20232  xkotf  20252  dfac14lem  20284  prdstps  20296  txindis  20301  tx1stc  20317  xkohaus  20320  xkoptsub  20321  cnmpt1st  20335  cnmpt2nd  20336  ptcmpfi  20480  filcon  20550  trfil1  20553  fin1aufil  20599  tgpconcompeqg  20776  tgpconcomp  20777  tsmsresOLD  20811  tsmsres  20812  trust  20898  met1stc  21190  dscmet  21259  nmoval  21388  retopon  21436  cnfldtopon  21456  xrsxmet  21480  xrsmopn  21483  metdsval  21517  iimulcn  21604  icopnfhmeo  21609  iccpnfhmeo  21611  xrhmeo  21612  cnheiborlem  21620  lebnumii  21632  ishtpy  21638  htpycc  21646  pco1  21681  pcohtpylem  21685  pcopt  21688  pcopt2  21689  pcoass  21690  pcorevlem  21692  cfilresi  21900  rrxcph  21990  ovolval  22051  ovolf  22059  ovoliunlem3  22081  ovolicc1  22093  ovolicc2  22099  volf  22106  ioorf  22148  dyadf  22166  dyadmbl  22175  vitalilem5  22187  vitali  22188  mbfimaopnlem  22228  mbflimsup  22239  0plef  22245  i1fima  22251  i1fima2  22252  i1fd  22254  itg1ge0  22259  itg10  22261  i1f1lem  22262  i1fadd  22268  i1fmul  22269  i1fmulc  22276  mbfi1fseqlem5  22292  itg2addlem  22331  reldv  22440  dvbsss  22472  dvef  22547  lhop1lem  22580  deg1fvi  22651  plypf1  22775  coeeulem  22787  coeeu  22788  vieta1lem2  22873  aannenlem3  22892  aalioulem3  22896  dvradcnv  22982  pserulm  22983  pserdvlem2  22989  abelthlem6  22997  sinhalfpilem  23022  sincos4thpi  23072  tan4thpi  23073  sincos6thpi  23074  pige3  23076  resinf1o  23089  tanord1  23090  tanregt0  23092  efabl  23103  relogrn  23115  dfrelog  23119  logneg  23141  logltb  23153  logcn  23196  logf1o2  23199  dvlog  23200  efopnlem2  23206  efopn  23207  logccv  23212  dvsqrt  23286  cxpcn3  23290  logblog  23331  angpined  23358  1cubr  23370  asinsin  23420  asin1  23422  reasinsin  23424  atan0  23436  atanbnd  23454  atan1  23456  log2cnv  23472  log2ublem3  23476  log2ub  23477  log2le1  23478  birthday  23482  amgmlem  23517  emcllem5  23527  emgt0  23534  harmonicbnd3  23535  ftalem3  23546  basellem4  23555  sgmf  23617  ppi1  23636  cht1  23637  vma1  23638  ppiltx  23649  sqff1o  23654  ppiublem1  23675  ppiublem2  23676  ppiub  23677  chtub  23685  dchreq  23731  bposlem7  23763  bposlem8  23764  bposlem9  23765  lgsdir2lem2  23797  lgsdir2lem3  23798  chebbnd1  23855  chto1ub  23859  chpo1ubb  23864  pntibndlem1  23972  tgldimor  24094  tglnfn  24135  axlowdimlem4  24450  axlowdimlem16  24462  axlowdim  24466  umgrafi  24524  usgraexmpl  24603  usgraexmplc  24606  usgrafilem1  24613  2trllemA  24754  wlkntrllem1  24763  wlkntrllem3  24765  0pth  24774  spthispth  24777  2pthon  24806  2pthon3v  24808  constr3trllem3  24854  constr3pthlem3  24859  konigsberg  25189  frgrawopreg2  25253  ex-dif  25346  ex-un  25347  ex-in  25348  ex-fl  25370  avril1  25373  ginvsn  25549  cnid  25551  mulid  25556  rngosn3  25626  vcoprnelem  25669  vcex  25671  cnnvm  25786  ipasslem8  25950  ipasslem10  25952  hvsubf  26130  normlem1  26225  normlem6  26230  normlem7  26231  norm-ii-i  26252  norm3adifii  26263  hilid  26276  hlimf  26353  hhssabloi  26376  hhssnv  26378  hhshsslem1  26381  shincli  26478  shsval2i  26503  shs0i  26565  chj0i  26571  chm1i  26572  chincli  26576  chdmm1i  26593  shjshsi  26608  chsup0  26664  h1de2bi  26670  spansnpji  26694  cmcmlem  26707  cmcmii  26713  cmcm2ii  26714  cmcm3ii  26715  pjidmi  26789  pjssmii  26797  pj0i  26809  pjocini  26814  mayetes3i  26846  df0op2  26869  hoaddcomi  26889  hoaddassi  26893  hocadddiri  26896  hocsubdiri  26897  hoaddid1i  26903  ho0coi  26905  hoid1i  26906  hoid1ri  26907  hodseqi  26911  honegsubi  26913  adj1o  27011  hoddii  27106  lnopunilem1  27127  lnopunilem2  27128  nmcopexi  27144  nmcopex  27146  nmcoplb  27147  nmcfnexi  27168  nmcfnex  27170  nmcfnlb  27171  adjbd1o  27202  adjcoi  27217  nmopcoadji  27218  opsqrlem6  27262  pjsdii  27272  pjddii  27273  pjidmcoi  27294  pjtoi  27296  pjin1i  27309  pjclem1  27312  stji1i  27359  reuxfr3d  27586  inindif  27613  iuninc  27638  fnresin  27689  rinvf1o  27691  suppss2f  27698  xppreima  27708  ofoprabco  27732  funcnvmptOLD  27736  gtiso  27747  df1stres  27750  df2ndres  27751  snct  27764  dmct  27767  padct  27776  ffsrn  27783  fpwrelmapffs  27788  xrge0infssd  27812  nnindf  27844  nn0min  27845  ressplusf  27872  xrsclat  27902  xrge0base  27907  xrge00  27908  xrge0neqmnf  27913  xrnarchi  27962  xrge0slmod  28069  locfinreflem  28078  locfinref  28079  unicls  28120  sqsscirc1  28125  mhmhmeotmd  28144  rmulccn  28145  raddcn  28146  xrge0iifiso  28152  xrge0iifhmeo  28153  lmxrge0  28169  cnzh  28185  rezh  28186  qqh0  28199  qqh1  28200  qqhre  28232  esumnul  28277  esum0  28278  esumsnf  28293  esumpfinvallem  28303  esumpfinvalf  28305  esumpcvgval  28307  esumcvgsum  28317  esumsup  28318  esumcvgre  28320  sigaclfu2  28351  dmsigagen  28374  ddemeas  28445  imambfm  28470  mbfmvolf  28474  br2base  28477  omsfval  28502  omsf  28504  oms0  28505  omssubaddlem  28507  omssubadd  28508  carsgclctunlem3  28528  sibfof  28546  sitg0  28552  eulerpartlemt  28574  eulerpartgbij  28575  0rrv  28654  coinfliplem  28681  coinflipprob  28682  coinfliprv  28685  ballotlem2  28691  ballotlem4  28701  ballotlem5  28702  ballotlemi1  28705  ballotlem7  28738  ballotth  28740  signsplypnf  28771  signsply0  28772  signsw0g  28777  signswch  28782  signsvf0  28801  subfacf  28883  subfacp1lem1  28887  subfacp1lem5  28892  subfacp1lem6  28893  subfacval3  28897  erdszelem2  28900  kur14lem4  28917  iooscon  28956  iccllyscon  28959  msrfo  29170  mthmpps  29206  problem5  29287  quad3  29288  ghomgrpilem1  29289  ghomgrpilem2  29290  circum  29304  axextprim  29314  axrepprim  29315  axunprim  29316  axinfprim  29319  axacprim  29320  inffz  29349  logi  29362  risefall0lem  29389  setinds  29450  dfon2lem2  29456  dfon2lem4  29458  axextdfeq  29470  poseq  29573  wfrlem4  29586  frrlem4  29630  nosgnn0  29658  sltsolem1  29668  bdayfo  29675  fobigcup  29778  snelsingles  29800  fullfunfnv  29824  fullfunfv  29825  rankaltopb  29857  rank0  30055  rankeq1o  30056  hfuni  30069  nabi1i  30085  nabi2i  30086  limsucncmpi  30138  tan2h  30287  mblfinlem1  30291  mblfinlem2  30292  ovoliunnfl  30296  voliunnfl  30298  dvtanlem  30304  itg2addnclem  30306  itg2addnclem2  30307  dvcnsqrt  30341  asindmre  30342  areacirclem1  30347  fneer  30411  neibastop1  30417  fdc  30478  cntotbnd  30532  heiborlem6  30552  rrnval  30563  reheibor  30575  prter2  30862  diophrw  30931  rabren3dioph  30988  pellexlem6  31009  pellex  31010  frmx  31088  frmy  31089  jm2.23  31177  jm2.27dlem3  31192  axac10  31214  pw2f1ocnv  31218  kelac2lem  31249  lmhmlnmsplit  31272  pwfi2f1o  31283  pwfi2f1oOLD  31284  frlmpwfi  31287  seff  31430  expgrowthi  31479  expgrowth  31481  binomcxplemnotnn0  31502  negpilt0  31702  ioontr  31788  iccdifioo  31794  iccdifprioo  31795  fsummulc1f  31808  icccncfext  31929  dvcosre  31945  dvsinax  31947  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  dvmptmulf  31973  dvnmul  31979  dvmptfprodlem  31980  dvnprodlem2  31983  stoweidlem1  32022  stoweidlem26  32047  stoweidlem34  32055  stoweidlem44  32065  stoweid  32084  stirlinglem5  32099  dirkercncflem1  32124  fourierdlem44  32172  fourierdlem56  32184  fourierdlem62  32190  fourierdlem89  32217  fourierdlem91  32219  fourierdlem100  32228  fourierdlem102  32230  fourierdlem103  32231  fourierdlem104  32232  fourierdlem108  32236  fourierdlem112  32240  fourierdlem114  32242  fouriersw  32253  axorbtnotaiffb  32337  axorbciffatcxorb  32339  abnotbtaxb  32350  1nevenALTV  32597  resisresindm  32679  residfi  32688  ldepslinc  33364  3halfnz  33380  alimp-no-surprise  33584  aacllem  33604  ee233  33676  ax6e2nd  33725  in1  33742  dfvd2ani  33754  dfvd2i  33756  dfvd3i  33763  dfvd3ani  33766  e0bi  33967  uun2221  34004  uun2221p1  34005  uun2221p2  34006  en3lpVD  34045  relopabVD  34102  ax6e2ndVD  34109  ax6e2ndALT  34131  bnj521  34193  bnj1098  34243  bnj1109  34246  bnj1131  34247  bnj1533  34311  bnj151  34336  bnj580  34372  bnj852  34380  bnj864  34381  bnj865  34382  bnj978  34408  bnj1021  34423  bnj907  34424  bnj1093  34437  bnj1145  34450  bnj1172  34458  bnj1174  34460  bnj1176  34462  bnj1186  34464  bj-nfxfr  34619  bj-axsep  34780  bj-zfpow  34782  bj-dtru  34784  bj-n0i  34904  bj-snsetex  34922  bj-tagss  34939  bj-2upln0  34982  bj-2upln1upl  34983  bj-nuliota  34987  bj-elid  35000  bj-pinftyccb  35024  bj-minftyccb  35028  bj-pinftynminfty  35030  renegclALT  35091  mapdunirnN  37774  ifpbiidcor  38141  iunrelexp0  38224  corcltrcl  38231  cotrclrcl  38232  0heALT  38256  frege54cor1a  38341  int-rightdistd  38453  int-sqdefd  38454  int-sqgeq0d  38459
  Copyright terms: Public domain W3C validator