ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbird Unicode version

Theorem mpbird 165
Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbird.min  |-  ( ph  ->  ch )
mpbird.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mpbird  |-  ( ph  ->  ps )

Proof of Theorem mpbird
StepHypRef Expression
1 mpbird.min . 2  |-  ( ph  ->  ch )
2 mpbird.maj . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
32biimprd 156 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mpd 13 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mpbiri  166  pm5.19  655  mpbir2and  886  pm3.12dc  900  mpbir3and  1122  pm5.15dc  1321  eqeltrd  2159  eqnetrd  2273  3netr4d  2282  sbcne12g  2934  eqsstrd  3043  3sstr4d  3052  eqbrtrd  3826  3brtr4d  3836  snelpwi  3996  prelpwi  3998  pwel  4002  ordelon  4167  onin  4170  elelsuc  4193  suceloni  4274  sucelon  4276  onintonm  4290  sosng  4460  relssdv  4479  eqbrrdv  4484  eqrelrdv2  4486  relsnopg  4491  breldmg  4590  iss  4705  xpimasn  4820  elxp4  4859  elxp5  4860  funssres  4993  sefvex  5248  fvun1  5292  eqfnfvd  5321  fvimacnvi  5334  fvimacnv  5335  fvelrn  5351  fmpt2d  5380  fmptco  5383  fsn  5388  ftpg  5400  fconst2g  5429  funfvima3  5445  foeqcnvco  5482  f1eqcocnv  5483  fliftfun  5488  fliftfund  5489  fliftval  5492  riota5f  5544  f1ofveu  5552  f1ocnvd  5754  f1opw2  5758  fnofval  5773  off  5776  offval2  5778  ofrfval2  5779  caofref  5784  caofinvl  5785  elxp6  5848  cnvf1olem  5897  f2ndf  5899  f1od2  5908  tposf12  5939  smores2  5964  tfrlemisucaccv  5995  tfrlemibfn  5998  tfr1onlemsucaccv  6011  tfr1onlembfn  6014  tfrcllemsucaccv  6024  tfrcllembfn  6027  tfrcl  6034  tfri3  6037  frecabcl  6069  nnsucsssuc  6157  ersym  6206  ertr  6209  swoer  6222  erth  6238  riinerm  6267  qliftfund  6277  eroprf  6287  ecopoverg  6295  th3qlem1  6296  f1dom2g  6325  dom3d  6343  fopwdom  6402  nndomo  6421  dif1en  6436  findcard2  6446  findcard2s  6447  diffisn  6450  fientri3  6460  f1dmvrnfibi  6485  supelti  6510  supsnti  6513  cnvinfex  6526  ordiso2  6541  isnumi  6546  ltsopi  6608  pitri3or  6610  ltdcpi  6611  indpi  6630  enqdc  6649  enqdc1  6650  addcmpblnq  6655  mulcanenq  6673  recrecnq  6682  nqtri3or  6684  ltdcnq  6685  ltsonq  6686  ltaddnq  6695  subhalfnqq  6702  archnqq  6705  prarloclemarch2  6707  enq0tr  6722  nqnq0  6729  addcmpblnq0  6731  mulcanenq0ec  6733  nnnq0lem1  6734  nqpnq0nq  6741  nq0m0r  6744  nq02m  6753  prarloclemlt  6781  prarloclemcalc  6790  addlocpr  6824  nqprl  6839  nqpru  6840  addnqprlemrl  6845  addnqprlemru  6846  prmuloclemcalc  6853  mullocprlem  6858  mulnqprlemrl  6861  mulnqprlemru  6862  1idprl  6878  1idpru  6879  ltaddpr  6885  ltexprlemm  6888  ltexprlemopl  6889  ltexprlemopu  6891  ltexprlemdisj  6894  ltexprlemrl  6898  ltexprlemru  6900  addcanprleml  6902  addcanprlemu  6903  addcanprg  6904  prplnqu  6908  recexprlemloc  6919  recexprlem1ssl  6921  recexprlem1ssu  6922  aptiprleml  6927  aptiprlemu  6928  archpr  6931  cauappcvgprlemm  6933  cauappcvgprlemopl  6934  cauappcvgprlemloc  6940  cauappcvgprlemladdfu  6942  cauappcvgprlemladdfl  6943  cauappcvgprlem1  6947  cauappcvgprlem2  6948  caucvgprlemnkj  6954  caucvgprlemopl  6957  caucvgprlemloc  6963  caucvgprlemladdfu  6965  caucvgprlem2  6968  caucvgprprlemnkltj  6977  caucvgprprlemopl  6985  caucvgprprlemloc  6991  caucvgprprlemexbt  6994  caucvgprprlemaddq  6996  caucvgprprlem2  6998  prsrlem1  7017  0idsr  7042  1idsr  7043  recexgt0sr  7048  archsr  7056  prsradd  7060  caucvgsrlemcau  7067  caucvgsrlembound  7068  caucvgsrlemoffgt1  7073  pitonnlem1p1  7112  pitonn  7114  pitoregt0  7115  peano2nnnn  7119  recidpirq  7124  axcaucvglemval  7161  leid  7298  nltled  7333  readdcan  7351  addneintrd  7399  addneintr2d  7400  pncan  7417  subsub2  7439  subsub4  7444  negned  7519  subne0d  7531  subneintrd  7566  subneintr2d  7568  subeq0bd  7586  subdi  7592  gt0add  7776  rimul  7788  rereim  7789  ltmul1a  7794  apreim  7806  apirr  7808  mulap0r  7818  msqge0  7819  mulge0  7822  gt0ap0  7828  ltap  7834  recexaplem2  7845  mulap0bad  7852  mulap0bbd  7853  divrecap  7879  div0ap  7893  div1  7894  recrecap  7900  divdivdivap  7904  ddcanap  7917  rerecclap  7921  div2negap  7926  recgt0  8031  prodgt0  8033  lemul1a  8039  recp1lt1  8080  squeeze0  8085  peano2nn  8154  div4p1lem1div2  8387  arch  8388  peano2z  8504  peano2zm  8506  ztri3or  8511  nn0n0n1ge2  8535  zextle  8555  gtndiv  8559  suprzclex  8562  nn0ind-raph  8581  uzid  8750  uzneg  8754  uztric  8757  uz11  8758  eluzp1l  8760  qdivcl  8845  irrmul  8849  rpnegap  8883  ledivge1le  8920  nn0ledivnn  8955  ltpnf  8968  mnflt  8970  pnfge  8976  mnfle  8979  xrlttr  8982  xrltso  8983  xrlttri3  8984  xrleid  8986  iccf1o  9138  fztri3or  9170  fznlem  9172  fzn  9173  fzsplit2  9181  fznatpl1  9205  uzsplit  9221  fseq1p1m1  9223  fzm1  9229  fznn0sub2  9252  difelfznle  9259  1fv  9262  fzospliti  9298  fzouzsplit  9301  eluzgtdifelfzo  9319  exfzdc  9362  subfzo0  9364  exbtwnz  9373  qbtwnrelemcalc  9378  flqlelt  9394  qfraclt1  9398  qfracge0  9399  flqltnz  9405  btwnzge0  9418  flhalf  9420  ceiqle  9431  intfracq  9438  mulqmod0  9448  modqge0  9450  modqlt  9451  modqid  9467  modqid0  9468  m1modge3gt1  9489  modqltm1p1mod  9494  q2txmodxeq0  9502  modaddmodlo  9506  modsumfzodifsn  9514  addmodlteq  9516  frecuzrdgtcl  9530  frecuzrdgtclt  9539  uzsinds  9554  iseqfclt  9572  iseqoveq  9576  monoord2  9588  iseqid3  9597  serile  9607  expivallem  9610  expival  9611  expp1  9616  expcllem  9620  ltexp2a  9661  leexp2a  9662  faclbnd  9801  faclbnd2  9802  faclbnd3  9803  ibcval5  9823  bcpasc  9826  hashennn  9840  fihasheqf1oi  9848  hashsng  9858  fihashfn  9860  hashun  9865  fihashss  9876  fihashssdif  9878  hashfz  9881  hashxp  9886  shftfn  9897  cjth  9918  cjmulrcl  9959  reim0bd  10016  rerebd  10017  cjrebd  10018  caucvgre  10052  cvg1nlemcxze  10053  cvg1nlemcau  10055  cvg1nlemres  10056  recvguniq  10066  resqrexlemover  10081  resqrexlemdec  10082  resqrexlemgt0  10091  resqrexlemoverl  10092  resqrexlemglsq  10093  rersqrtthlem  10101  sqrtgt0  10105  leabs  10145  absexpzap  10151  absle  10160  recvalap  10168  abstri  10175  abs2dif  10177  amgm2  10189  absne0d  10258  maxleim  10276  maxabslemab  10277  maxabslemlub  10278  maxltsup  10289  fimaxre2  10294  minmax  10297  climconst  10314  climuni  10317  2clim  10325  climcn1  10332  climcn2  10333  climge0  10348  climle  10357  climsqz  10358  climsqz2  10359  serif0  10374  dvdsval2  10390  dvdsdc  10395  dvds0lem  10397  zdvdsdc  10408  dvdscmulr  10416  dvdsmulcr  10417  dvdslelemd  10435  divconjdvds  10441  dvdsext  10447  fzm1ndvds  10448  dvdsmod  10454  oexpneg  10468  2tp1odd  10475  mulsucdiv2z  10476  2teven  10478  zeo5  10479  opeo  10488  omeo  10489  nn0ob  10499  divalglemnqt  10511  zsupcllemstep  10532  zsupcl  10534  zssinfcl  10535  infssuzex  10536  infssuzcldc  10538  gcddvds  10546  dvdslegcd  10547  gcdneg  10564  bezoutlemnewy  10576  bezoutlemstep  10577  bezoutlema  10579  bezoutlemb  10580  bezoutlemmo  10586  bezoutlemle  10588  bezoutlemsup  10589  dfgcd3  10590  bezout  10591  dfgcd2  10594  lcmcllem  10640  lcmneg  10647  lcmgcdlem  10650  lcmdvds  10652  lcmid  10653  3lcm2e6woprm  10659  6lcm4e12  10660  ncoprmgcdne1b  10662  mulgcddvds  10667  divgcdcoprmex  10675  cncongr1  10676  cncongr2  10677  isprm2lem  10689  prmind2  10693  dvdsnprmd  10698  prm2orodd  10699  sqnprm  10708  rpexp  10723  sqrt2irrlem  10731  oddpwdclemdc  10742  sqrt2irraplemnn  10748  qnumdencoprm  10762  qeqnumdivden  10763  nn0gcdsq  10769  nn0sqrtelqelz  10775  nonsq  10776  phicl2  10781  phibnd  10784  hashdvds  10788  phiprmpw  10789  phimullem  10792  hashgcdlem  10794  znnen  10802  bj-sels  10956  bj-nnelon  11005
  Copyright terms: Public domain W3C validator