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

Theorem mpbird 156
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 147 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mpd 13 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpbiri  157  pm5.19  622  mpbir2and  851  pm3.12dc  865  mpbir3and  1087  pm5.15dc  1280  eqeltrd  2114  eqnetrd  2229  3netr4d  2238  sbcne12g  2868  eqsstrd  2979  3sstr4d  2988  eqbrtrd  3784  3brtr4d  3794  snelpwi  3948  prelpwi  3950  pwel  3954  ordelon  4120  onin  4123  elelsuc  4146  suceloni  4227  sucelon  4229  onintonm  4243  sosng  4413  relssdv  4432  eqbrrdv  4437  eqrelrdv2  4439  breldmg  4541  iss  4654  xpimasn  4769  elxp4  4808  elxp5  4809  funssres  4942  sefvex  5196  fvun1  5239  eqfnfvd  5268  fvimacnvi  5281  fvimacnv  5282  fvelrn  5298  fmpt2d  5327  fmptco  5330  fsn  5335  ftpg  5347  fconst2g  5376  funfvima3  5392  foeqcnvco  5430  f1eqcocnv  5431  fliftfun  5436  fliftfund  5437  fliftval  5440  riota5f  5492  f1ofveu  5500  f1ocnvd  5702  f1opw2  5706  fnofval  5721  off  5724  offval2  5726  ofrfval2  5727  caofref  5732  caofinvl  5733  elxp6  5796  cnvf1olem  5845  f2ndf  5847  tposf12  5884  smores2  5909  tfrlemisucaccv  5939  tfrlemibfn  5942  tfri3  5953  frecsuclemdm  5988  nnsucsssuc  6071  ersym  6118  ertr  6121  swoer  6134  erth  6150  riinerm  6179  qliftfund  6189  eroprf  6199  ecopoverg  6207  th3qlem1  6208  f1dom2g  6236  dom3d  6254  fopwdom  6310  nndomo  6326  dif1en  6337  findcard2  6346  findcard2s  6347  diffisn  6350  fientri3  6353  ordiso2  6357  isnumi  6362  ltsopi  6418  pitri3or  6420  ltdcpi  6421  indpi  6440  enqdc  6459  enqdc1  6460  addcmpblnq  6465  mulcanenq  6483  recrecnq  6492  nqtri3or  6494  ltdcnq  6495  ltsonq  6496  ltaddnq  6505  subhalfnqq  6512  archnqq  6515  prarloclemarch2  6517  enq0tr  6532  nqnq0  6539  addcmpblnq0  6541  mulcanenq0ec  6543  nnnq0lem1  6544  nqpnq0nq  6551  nq0m0r  6554  nq02m  6563  prarloclemlt  6591  prarloclemcalc  6600  addlocpr  6634  nqprl  6649  nqpru  6650  addnqprlemrl  6655  addnqprlemru  6656  prmuloclemcalc  6663  mullocprlem  6668  mulnqprlemrl  6671  mulnqprlemru  6672  1idprl  6688  1idpru  6689  ltaddpr  6695  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemdisj  6704  ltexprlemrl  6708  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  addcanprg  6714  prplnqu  6718  recexprlemloc  6729  recexprlem1ssl  6731  recexprlem1ssu  6732  aptiprleml  6737  aptiprlemu  6738  archpr  6741  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemloc  6750  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlem1  6757  cauappcvgprlem2  6758  caucvgprlemnkj  6764  caucvgprlemopl  6767  caucvgprlemloc  6773  caucvgprlemladdfu  6775  caucvgprlem2  6778  caucvgprprlemnkltj  6787  caucvgprprlemopl  6795  caucvgprprlemloc  6801  caucvgprprlemexbt  6804  caucvgprprlemaddq  6806  caucvgprprlem2  6808  prsrlem1  6827  0idsr  6852  1idsr  6853  recexgt0sr  6858  archsr  6866  prsradd  6870  caucvgsrlemcau  6877  caucvgsrlembound  6878  caucvgsrlemoffgt1  6883  pitonnlem1p1  6922  pitonn  6924  pitoregt0  6925  peano2nnnn  6929  recidpirq  6934  axcaucvglemval  6971  leid  7102  readdcan  7153  addneintrd  7199  addneintr2d  7200  pncan  7217  subsub2  7239  subsub4  7244  negned  7319  subne0d  7331  subneintrd  7366  subneintr2d  7368  subeq0bd  7377  subdi  7382  gt0add  7564  rimul  7576  rereim  7577  ltmul1a  7582  apreim  7594  apirr  7596  mulap0r  7606  msqge0  7607  mulge0  7610  gt0ap0  7616  ltap  7622  recexaplem2  7633  mulap0bad  7640  mulap0bbd  7641  divrecap  7667  div0ap  7679  div1  7680  recrecap  7685  divdivdivap  7689  ddcanap  7702  rerecclap  7706  div2negap  7711  recgt0  7816  prodgt0  7818  lemul1a  7824  recp1lt1  7865  squeeze0  7870  peano2nn  7926  div4p1lem1div2  8177  arch  8178  peano2z  8281  peano2zm  8283  ztri3or  8288  nn0n0n1ge2  8311  zextle  8331  gtndiv  8335  nn0ind-raph  8355  uzid  8487  uzneg  8491  uztric  8494  uz11  8495  eluzp1l  8497  qdivcl  8577  irrmul  8581  rpnegap  8615  ledivge1le  8652  ltpnf  8702  mnflt  8704  pnfge  8710  mnfle  8713  xrlttr  8716  xrltso  8717  xrlttri3  8718  xrleid  8720  iccf1o  8872  fztri3or  8903  fznlem  8905  fzn  8906  fzsplit2  8914  fznatpl1  8938  uzsplit  8954  fseq1p1m1  8956  fzm1  8962  fznn0sub2  8985  difelfznle  8993  1fv  8996  fzospliti  9032  fzouzsplit  9035  eluzgtdifelfzo  9053  subfzo0  9097  qbtwnz  9106  qbtwnrelemcalc  9110  flqlelt  9118  qfraclt1  9122  qfracge0  9123  flqltnz  9129  btwnzge0  9142  flhalf  9144  ceiqle  9155  intfracq  9162  mulqmod0  9172  modqge0  9174  modqlt  9175  frecuzrdgfn  9198  monoord2  9236  iseqid3  9245  serile  9253  expivallem  9256  expival  9257  expp1  9262  expcllem  9266  ltexp2a  9306  leexp2a  9307  shftfn  9425  cjth  9446  cjmulrcl  9487  reim0bd  9544  rerebd  9545  cjrebd  9546  caucvgre  9580  cvg1nlemcxze  9581  cvg1nlemcau  9583  cvg1nlemres  9584  recvguniq  9593  resqrexlemover  9608  resqrexlemdec  9609  resqrexlemgt0  9618  resqrexlemoverl  9619  resqrexlemglsq  9620  rersqrtthlem  9628  sqrtgt0  9632  leabs  9672  absexpzap  9676  absle  9685  recvalap  9693  abstri  9700  abs2dif  9702  amgm2  9714  absne0d  9783  climconst  9811  climuni  9814  2clim  9822  climcn1  9829  climcn2  9830  climge0  9845  climle  9854  climsqz  9855  climsqz2  9856  serif0  9871  sqr2irrlem  9877  bj-sels  10034  bj-nnelon  10084
  Copyright terms: Public domain W3C validator