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

Theorem mpbird 160
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 151 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mpd 13 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  mpbiri  161  pm5.19  632  mpbir2and  862  pm3.12dc  876  mpbir3and  1098  pm5.15dc  1296  eqeltrd  2130  eqnetrd  2244  3netr4d  2253  sbcne12g  2895  eqsstrd  3006  3sstr4d  3015  eqbrtrd  3811  3brtr4d  3821  snelpwi  3975  prelpwi  3977  pwel  3981  ordelon  4147  onin  4150  elelsuc  4173  suceloni  4254  sucelon  4256  onintonm  4270  sosng  4440  relssdv  4459  eqbrrdv  4464  eqrelrdv2  4466  breldmg  4568  iss  4681  xpimasn  4796  elxp4  4835  elxp5  4836  funssres  4969  sefvex  5223  fvun1  5266  eqfnfvd  5295  fvimacnvi  5308  fvimacnv  5309  fvelrn  5325  fmpt2d  5354  fmptco  5357  fsn  5362  ftpg  5374  fconst2g  5403  funfvima3  5419  foeqcnvco  5457  f1eqcocnv  5458  fliftfun  5463  fliftfund  5464  fliftval  5467  riota5f  5519  f1ofveu  5527  f1ocnvd  5729  f1opw2  5733  fnofval  5748  off  5751  offval2  5753  ofrfval2  5754  caofref  5759  caofinvl  5760  elxp6  5823  cnvf1olem  5872  f2ndf  5874  f1od2  5883  tposf12  5914  smores2  5939  tfrlemisucaccv  5969  tfrlemibfn  5972  tfri3  5983  frecsuclemdm  6018  nnsucsssuc  6101  ersym  6148  ertr  6151  swoer  6164  erth  6180  riinerm  6209  qliftfund  6219  eroprf  6229  ecopoverg  6237  th3qlem1  6238  f1dom2g  6266  dom3d  6284  fopwdom  6340  nndomo  6356  dif1en  6367  findcard2  6376  findcard2s  6377  diffisn  6380  fientri3  6383  supsnti  6408  ordiso2  6414  isnumi  6419  ltsopi  6475  pitri3or  6477  ltdcpi  6478  indpi  6497  enqdc  6516  enqdc1  6517  addcmpblnq  6522  mulcanenq  6540  recrecnq  6549  nqtri3or  6551  ltdcnq  6552  ltsonq  6553  ltaddnq  6562  subhalfnqq  6569  archnqq  6572  prarloclemarch2  6574  enq0tr  6589  nqnq0  6596  addcmpblnq0  6598  mulcanenq0ec  6600  nnnq0lem1  6601  nqpnq0nq  6608  nq0m0r  6611  nq02m  6620  prarloclemlt  6648  prarloclemcalc  6657  addlocpr  6691  nqprl  6706  nqpru  6707  addnqprlemrl  6712  addnqprlemru  6713  prmuloclemcalc  6720  mullocprlem  6725  mulnqprlemrl  6728  mulnqprlemru  6729  1idprl  6745  1idpru  6746  ltaddpr  6752  ltexprlemm  6755  ltexprlemopl  6756  ltexprlemopu  6758  ltexprlemdisj  6761  ltexprlemrl  6765  ltexprlemru  6767  addcanprleml  6769  addcanprlemu  6770  addcanprg  6771  prplnqu  6775  recexprlemloc  6786  recexprlem1ssl  6788  recexprlem1ssu  6789  aptiprleml  6794  aptiprlemu  6795  archpr  6798  cauappcvgprlemm  6800  cauappcvgprlemopl  6801  cauappcvgprlemloc  6807  cauappcvgprlemladdfu  6809  cauappcvgprlemladdfl  6810  cauappcvgprlem1  6814  cauappcvgprlem2  6815  caucvgprlemnkj  6821  caucvgprlemopl  6824  caucvgprlemloc  6830  caucvgprlemladdfu  6832  caucvgprlem2  6835  caucvgprprlemnkltj  6844  caucvgprprlemopl  6852  caucvgprprlemloc  6858  caucvgprprlemexbt  6861  caucvgprprlemaddq  6863  caucvgprprlem2  6865  prsrlem1  6884  0idsr  6909  1idsr  6910  recexgt0sr  6915  archsr  6923  prsradd  6927  caucvgsrlemcau  6934  caucvgsrlembound  6935  caucvgsrlemoffgt1  6940  pitonnlem1p1  6979  pitonn  6981  pitoregt0  6982  peano2nnnn  6986  recidpirq  6991  axcaucvglemval  7028  leid  7160  nltled  7195  readdcan  7213  addneintrd  7261  addneintr2d  7262  pncan  7279  subsub2  7301  subsub4  7306  negned  7381  subne0d  7393  subneintrd  7428  subneintr2d  7430  subeq0bd  7448  subdi  7453  gt0add  7637  rimul  7649  rereim  7650  ltmul1a  7655  apreim  7667  apirr  7669  mulap0r  7679  msqge0  7680  mulge0  7683  gt0ap0  7689  ltap  7695  recexaplem2  7706  mulap0bad  7713  mulap0bbd  7714  divrecap  7740  div0ap  7752  div1  7753  recrecap  7759  divdivdivap  7763  ddcanap  7776  rerecclap  7780  div2negap  7785  recgt0  7890  prodgt0  7892  lemul1a  7898  recp1lt1  7939  squeeze0  7944  peano2nn  8001  div4p1lem1div2  8234  arch  8235  peano2z  8337  peano2zm  8339  ztri3or  8344  nn0n0n1ge2  8368  zextle  8388  gtndiv  8392  nn0ind-raph  8413  uzid  8582  uzneg  8586  uztric  8589  uz11  8590  eluzp1l  8592  qdivcl  8674  irrmul  8678  rpnegap  8712  ledivge1le  8749  nn0ledivnn  8784  ltpnf  8802  mnflt  8804  pnfge  8810  mnfle  8813  xrlttr  8816  xrltso  8817  xrlttri3  8818  xrleid  8820  iccf1o  8972  fztri3or  9004  fznlem  9006  fzn  9007  fzsplit2  9015  fznatpl1  9039  uzsplit  9055  fseq1p1m1  9057  fzm1  9063  fznn0sub2  9086  difelfznle  9094  1fv  9097  fzospliti  9133  fzouzsplit  9136  eluzgtdifelfzo  9154  subfzo0  9198  qbtwnz  9207  qbtwnrelemcalc  9211  flqlelt  9220  qfraclt1  9224  qfracge0  9225  flqltnz  9231  btwnzge0  9244  flhalf  9246  ceiqle  9257  intfracq  9264  mulqmod0  9274  modqge0  9276  modqlt  9277  modqid  9293  modqid0  9294  m1modge3gt1  9315  modqltm1p1mod  9320  q2txmodxeq0  9328  modaddmodlo  9332  modsumfzodifsn  9340  addmodlteq  9342  frecuzrdgfn  9356  monoord2  9394  iseqid3  9403  serile  9412  expivallem  9415  expival  9416  expp1  9421  expcllem  9425  ltexp2a  9466  leexp2a  9467  faclbnd  9602  faclbnd2  9603  faclbnd3  9604  ibcval5  9624  bcpasc  9627  shftfn  9646  cjth  9667  cjmulrcl  9708  reim0bd  9765  rerebd  9766  cjrebd  9767  caucvgre  9801  cvg1nlemcxze  9802  cvg1nlemcau  9804  cvg1nlemres  9805  recvguniq  9814  resqrexlemover  9829  resqrexlemdec  9830  resqrexlemgt0  9839  resqrexlemoverl  9840  resqrexlemglsq  9841  rersqrtthlem  9849  sqrtgt0  9853  leabs  9893  absexpzap  9899  absle  9908  recvalap  9916  abstri  9923  abs2dif  9925  amgm2  9937  absne0d  10006  climconst  10034  climuni  10037  2clim  10045  climcn1  10052  climcn2  10053  climge0  10068  climle  10077  climsqz  10078  climsqz2  10079  serif0  10094  dvdsval2  10103  dvdsdc  10108  dvds0lem  10110  dvdscmulr  10128  dvdsmulcr  10129  dvdslelemd  10147  divconjdvds  10153  dvdsext  10159  fzm1ndvds  10160  dvdsmod  10166  oexpneg  10180  2tp1odd  10188  mulsucdiv2z  10189  2teven  10191  zeo5  10192  opeo  10201  omeo  10202  nn0ob  10212  sqr2irrlem  10222  oddpwdclemdc  10233  bj-sels  10393  bj-nnelon  10443
  Copyright terms: Public domain W3C validator