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

Step	Hyp	Ref	Expression
1		mpbird.min	. 2 |- ( ph -> ch )
2		mpbird.maj	. . 3 |- ( ph -> ( ps <-> ch ) )
3	2	biimprd 156	. 2 |- ( ph -> ( ch -> ps ) )
4	1, 3	mpd 13	1 |- ( ph -> ps )

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  888  pm3.12dc  902  mpbir3and  1124  pm5.15dc  1323  eqeltrd  2161  eqnetrd  2275  3netr4d  2284  sbcne12g  2938  eqsstrd  3049  3sstr4d  3058  eqbrtrd  3842  3brtr4d  3852  snelpwi  4015  prelpwi  4017  pwel  4021  ordelon  4186  onin  4189  elelsuc  4212  suceloni  4293  sucelon  4295  onintonm  4309  omsinds  4410  sosng  4481  relssdv  4500  eqbrrdv  4505  eqrelrdv2  4507  relsnopg  4512  breldmg  4612  iss  4727  xpimasn  4847  elxp4  4886  elxp5  4887  funssres  5023  f0rn0  5170  sefvex  5291  fvun1  5335  eqfnfvd  5365  fvimacnvi  5378  fvimacnv  5379  fvelrn  5395  fmpt3d  5419  fmpt2d  5425  resflem  5427  fmptco  5429  fsn  5434  ftpg  5446  fconst2g  5475  funfvima3  5491  foeqcnvco  5532  f1eqcocnv  5533  fliftfun  5538  fliftfund  5539  fliftval  5542  riota5f  5595  f1ofveu  5603  f1ocnvd  5805  f1opw2  5809  fnofval  5824  off  5827  offval2  5829  ofrfval2  5830  caofref  5835  caofinvl  5836  elxp6  5899  cnvf1olem  5948  f2ndf  5950  f1od2  5959  tposf12  5990  smores2  6015  tfrlemisucaccv  6046  tfrlemibfn  6049  tfr1onlemsucaccv  6062  tfr1onlembfn  6065  tfrcllemsucaccv  6075  tfrcllembfn  6078  tfrcl  6085  tfri3  6088  frecabcl  6120  nnsucsssuc  6209  ersym  6258  ertr  6261  swoer  6274  erth  6290  riinerm  6319  qliftfund  6329  eroprf  6339  ecopoverg  6347  th3qlem1  6348  elmapssres  6384  mapss  6402  fdiagfn  6403  f1dom2g  6427  dom3d  6445  fopwdom  6506  mapxpen  6518  nndomo  6534  dif1en  6549  findcard2  6559  findcard2s  6560  diffisn  6563  fimax2gtrilemstep  6570  fientri3  6579  f1dmvrnfibi  6606  sbthlemi6  6618  supelti  6644  supsnti  6647  cnvinfex  6660  ordiso2  6675  djuun  6707  updjud  6720  djudom  6734  enomnilem  6741  fodjuomnilemf  6747  isnumi  6757  exmidfodomrlemrALT  6776  ltsopi  6826  pitri3or  6828  ltdcpi  6829  indpi  6848  enqdc  6867  enqdc1  6868  addcmpblnq  6873  mulcanenq  6891  recrecnq  6900  nqtri3or  6902  ltdcnq  6903  ltsonq  6904  ltaddnq  6913  subhalfnqq  6920  archnqq  6923  prarloclemarch2  6925  enq0tr  6940  nqnq0  6947  addcmpblnq0  6949  mulcanenq0ec  6951  nnnq0lem1  6952  nqpnq0nq  6959  nq0m0r  6962  nq02m  6971  prarloclemlt  6999  prarloclemcalc  7008  addlocpr  7042  nqprl  7057  nqpru  7058  addnqprlemrl  7063  addnqprlemru  7064  prmuloclemcalc  7071  mullocprlem  7076  mulnqprlemrl  7079  mulnqprlemru  7080  1idprl  7096  1idpru  7097  ltaddpr  7103  ltexprlemm  7106  ltexprlemopl  7107  ltexprlemopu  7109  ltexprlemdisj  7112  ltexprlemrl  7116  ltexprlemru  7118  addcanprleml  7120  addcanprlemu  7121  addcanprg  7122  prplnqu  7126  recexprlemloc  7137  recexprlem1ssl  7139  recexprlem1ssu  7140  aptiprleml  7145  aptiprlemu  7146  archpr  7149  cauappcvgprlemm  7151  cauappcvgprlemopl  7152  cauappcvgprlemloc  7158  cauappcvgprlemladdfu  7160  cauappcvgprlemladdfl  7161  cauappcvgprlem1  7165  cauappcvgprlem2  7166  caucvgprlemnkj  7172  caucvgprlemopl  7175  caucvgprlemloc  7181  caucvgprlemladdfu  7183  caucvgprlem2  7186  caucvgprprlemnkltj  7195  caucvgprprlemopl  7203  caucvgprprlemloc  7209  caucvgprprlemexbt  7212  caucvgprprlemaddq  7214  caucvgprprlem2  7216  prsrlem1  7235  0idsr  7260  1idsr  7261  recexgt0sr  7266  archsr  7274  prsradd  7278  caucvgsrlemcau  7285  caucvgsrlembound  7286  caucvgsrlemoffgt1  7291  pitonnlem1p1  7330  pitonn  7332  pitoregt0  7333  peano2nnnn  7337  recidpirq  7342  axcaucvglemval  7379  leid  7516  nltled  7551  readdcan  7569  addneintrd  7617  addneintr2d  7618  pncan  7635  subsub2  7657  subsub4  7662  negned  7737  subne0d  7749  subneintrd  7784  subneintr2d  7786  subeq0bd  7804  subdi  7810  gt0add  7994  rimul  8006  rereim  8007  ltmul1a  8012  apreim  8024  apirr  8026  mulap0r  8036  msqge0  8037  mulge0  8040  gt0ap0  8046  ltap  8052  recexaplem2  8063  mulap0bad  8070  mulap0bbd  8071  divrecap  8097  div0ap  8111  div1  8112  recrecap  8118  divdivdivap  8122  ddcanap  8135  rerecclap  8139  div2negap  8144  recgt0  8249  prodgt0  8251  lemul1a  8257  recp1lt1  8298  squeeze0  8303  peano2nn  8372  div4p1lem1div2  8605  arch  8606  peano2z  8722  peano2zm  8724  ztri3or  8729  nn0n0n1ge2  8753  zextle  8773  gtndiv  8777  suprzclex  8780  nn0ind-raph  8799  uzid  8968  uzneg  8972  uztric  8975  uz11  8976  eluzp1l  8978  qdivcl  9063  irrmul  9067  rpnegap  9101  ledivge1le  9138  nn0ledivnn  9173  ltpnf  9186  mnflt  9188  pnfge  9194  mnfle  9197  xrlttr  9200  xrltso  9201  xrlttri3  9202  xrleid  9204  iccf1o  9356  fztri3or  9388  fznlem  9390  fzn  9391  fzsplit2  9399  fznatpl1  9423  uzsplit  9439  fseq1p1m1  9441  fzm1  9447  fznn0sub2  9470  difelfznle  9477  1fv  9481  fzodcel  9494  fzospliti  9518  fzouzsplit  9521  eluzgtdifelfzo  9539  exfzdc  9582  subfzo0  9584  exbtwnz  9593  qbtwnrelemcalc  9598  flqlelt  9614  qfraclt1  9618  qfracge0  9619  flqltnz  9625  btwnzge0  9638  flhalf  9640  ceiqle  9651  intfracq  9658  mulqmod0  9668  modqge0  9670  modqlt  9671  modqid  9687  modqid0  9688  m1modge3gt1  9709  modqltm1p1mod  9714  q2txmodxeq0  9722  modaddmodlo  9726  modsumfzodifsn  9734  addmodlteq  9736  frecuzrdgtcl  9750  frecuzrdgtclt  9759  uzsinds  9779  iseqfclt  9809  iseqoveq  9816  monoord2  9830  iseqf1olemqk  9847  iseqf1olemjpcl  9848  iseqf1olemqpcl  9849  iseqf1olemqsumkj  9851  iseqf1olemqsum  9853  iseqf1olemstep  9854  iseqf1oleml  9856  iseqid3  9860  ser3le  9873  expivallem  9876  expival  9877  expp1  9882  expcllem  9886  ltexp2a  9927  leexp2a  9928  faclbnd  10067  faclbnd2  10068  faclbnd3  10069  ibcval5  10089  bcpasc  10092  hashennn  10106  fihasheqf1oi  10114  hashsng  10124  fihashfn  10126  hashun  10131  fihashss  10142  fihashssdif  10144  hashfz  10147  hashxp  10152  fimaxq  10153  zfz1isolem1  10163  iseqcoll  10165  shftfn  10176  cjth  10197  cjmulrcl  10238  reim0bd  10295  rerebd  10296  cjrebd  10297  caucvgre  10331  cvg1nlemcxze  10332  cvg1nlemcau  10334  cvg1nlemres  10335  recvguniq  10345  resqrexlemover  10360  resqrexlemdec  10361  resqrexlemgt0  10370  resqrexlemoverl  10371  resqrexlemglsq  10372  rersqrtthlem  10380  sqrtgt0  10384  leabs  10424  absexpzap  10430  absle  10439  recvalap  10447  abstri  10454  abs2dif  10456  amgm2  10468  absne0d  10537  maxleim  10555  maxabslemab  10556  maxabslemlub  10557  maxltsup  10568  zmaxcl  10573  fimaxre2  10574  minmax  10577  climconst  10594  climuni  10597  2clim  10605  climcn1  10613  climcn2  10614  climge0  10629  climle  10638  climsqz  10639  climsqz2  10640  serif0  10655  isummolem3  10683  isummolem2a  10684  fsumcl2lem  10699  sumpr  10713  sumtp  10714  dvdsval2  10724  dvdsdc  10729  dvds0lem  10731  zdvdsdc  10742  dvdscmulr  10750  dvdsmulcr  10751  dvdslelemd  10769  divconjdvds  10775  dvdsext  10781  fzm1ndvds  10782  dvdsmod  10788  oexpneg  10802  2tp1odd  10809  mulsucdiv2z  10810  2teven  10812  zeo5  10813  opeo  10822  omeo  10823  nn0ob  10833  divalglemnqt  10845  zsupcllemstep  10866  zsupcl  10868  zssinfcl  10869  infssuzex  10870  infssuzcldc  10872  gcddvds  10880  dvdslegcd  10881  gcdneg  10898  bezoutlemnewy  10910  bezoutlemstep  10911  bezoutlema  10913  bezoutlemb  10914  bezoutlemmo  10920  bezoutlemle  10922  bezoutlemsup  10923  dfgcd3  10924  bezout  10925  dfgcd2  10928  lcmcllem  10974  lcmneg  10981  lcmgcdlem  10984  lcmdvds  10986  lcmid  10987  3lcm2e6woprm  10993  6lcm4e12  10994  ncoprmgcdne1b  10996  mulgcddvds  11001  divgcdcoprmex  11009  cncongr1  11010  cncongr2  11011  isprm2lem  11023  prmind2  11027  dvdsnprmd  11032  prm2orodd  11033  sqnprm  11042  rpexp  11057  sqrt2irrlem  11065  oddpwdclemdc  11076  sqrt2irraplemnn  11082  qnumdencoprm  11096  qeqnumdivden  11097  nn0gcdsq  11103  nn0sqrtelqelz  11109  nonsq  11110  phicl2  11115  phibnd  11118  hashdvds  11122  phiprmpw  11123  phimullem  11126  hashgcdlem  11128  znnen  11136  bj-sels  11293  bj-nnelon  11342  nninfall  11388  nninfsellemdc  11390  nninfself  11393