Theorem mpbird 166

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 157	. 2 |- ( ph -> ( ch -> ps ) )
4	1, 3	mpd 13	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbiri  167  pm5.19  663  mpbir2and  896  pm3.12dc  910  mpbir3and  1132  pm5.15dc  1335  eqeltrd  2176  eqnetrd  2291  3netr4d  2300  sbcne12g  2971  eqsstrd  3083  3sstr4d  3092  eqbrtrd  3895  3brtr4d  3905  snelpwi  4072  prelpwi  4074  pwel  4078  ordelon  4243  onin  4246  elelsuc  4269  suceloni  4355  sucelon  4357  onintonm  4371  omsinds  4473  sosng  4550  relssdv  4569  eqbrrdv  4574  eqrelrdv2  4576  relsnopg  4581  breldmg  4683  iss  4801  xpimasn  4923  elxp4  4962  elxp5  4963  funssres  5101  f0rn0  5253  sefvex  5374  fvun1  5419  eqfnfvd  5453  fvimacnvi  5466  fvimacnv  5467  fvelrn  5483  fmpt3d  5508  fmpt2d  5514  resflem  5516  fmptco  5518  fsn  5524  ftpg  5536  fconst2g  5567  funfvima3  5583  foeqcnvco  5623  f1eqcocnv  5624  fliftfun  5629  fliftfund  5630  fliftval  5633  riota5f  5686  f1ofveu  5694  f1ocnvd  5904  f1opw2  5908  fnofval  5923  off  5926  offval2  5928  ofrfval2  5929  caofref  5934  caofinvl  5935  elxp6  5998  cnvf1olem  6051  f2ndf  6053  f1od2  6062  tposf12  6096  smores2  6121  tfrlemisucaccv  6152  tfrlemibfn  6155  tfr1onlemsucaccv  6168  tfr1onlembfn  6171  tfrcllemsucaccv  6181  tfrcllembfn  6184  tfrcl  6191  tfri3  6194  frecabcl  6226  nnsucsssuc  6318  ersym  6371  ertr  6374  swoer  6387  erth  6403  riinerm  6432  qliftfund  6442  eroprf  6452  ecopoverg  6460  th3qlem1  6461  elmapssres  6497  mapss  6515  fdiagfn  6516  ixpssmap2g  6551  mapsnf1o  6561  f1dom2g  6580  dom3d  6598  fopwdom  6659  mapxpen  6671  nndomo  6687  dif1en  6702  findcard2  6712  findcard2s  6713  diffisn  6716  fimax2gtrilemstep  6723  fientri3  6732  fiintim  6746  f1dmvrnfibi  6760  sbthlemi6  6778  supelti  6804  supsnti  6807  cnvinfex  6820  ordiso2  6835  updjud  6882  djudom  6893  difinfsn  6900  ctssdc  6912  enumctlemm  6913  enumct  6914  enomnilem  6922  fodjuf  6929  omnimkv  6941  isnumi  6949  exmidfodomrlemrALT  6968  djudoml  6979  djudomr  6980  ltsopi  7029  pitri3or  7031  ltdcpi  7032  indpi  7051  enqdc  7070  enqdc1  7071  addcmpblnq  7076  mulcanenq  7094  recrecnq  7103  nqtri3or  7105  ltdcnq  7106  ltsonq  7107  ltaddnq  7116  subhalfnqq  7123  archnqq  7126  prarloclemarch2  7128  enq0tr  7143  nqnq0  7150  addcmpblnq0  7152  mulcanenq0ec  7154  nnnq0lem1  7155  nqpnq0nq  7162  nq0m0r  7165  nq02m  7174  prarloclemlt  7202  prarloclemcalc  7211  addlocpr  7245  nqprl  7260  nqpru  7261  addnqprlemrl  7266  addnqprlemru  7267  prmuloclemcalc  7274  mullocprlem  7279  mulnqprlemrl  7282  mulnqprlemru  7283  1idprl  7299  1idpru  7300  ltaddpr  7306  ltexprlemm  7309  ltexprlemopl  7310  ltexprlemopu  7312  ltexprlemdisj  7315  ltexprlemrl  7319  ltexprlemru  7321  addcanprleml  7323  addcanprlemu  7324  addcanprg  7325  prplnqu  7329  recexprlemloc  7340  recexprlem1ssl  7342  recexprlem1ssu  7343  aptiprleml  7348  aptiprlemu  7349  archpr  7352  cauappcvgprlemm  7354  cauappcvgprlemopl  7355  cauappcvgprlemloc  7361  cauappcvgprlemladdfu  7363  cauappcvgprlemladdfl  7364  cauappcvgprlem1  7368  cauappcvgprlem2  7369  caucvgprlemnkj  7375  caucvgprlemopl  7378  caucvgprlemloc  7384  caucvgprlemladdfu  7386  caucvgprlem2  7389  caucvgprprlemnkltj  7398  caucvgprprlemopl  7406  caucvgprprlemloc  7412  caucvgprprlemexbt  7415  caucvgprprlemaddq  7417  caucvgprprlem2  7419  prsrlem1  7438  0idsr  7463  1idsr  7464  recexgt0sr  7469  archsr  7477  prsradd  7481  caucvgsrlemcau  7488  caucvgsrlembound  7489  caucvgsrlemoffgt1  7494  pitonnlem1p1  7533  pitonn  7535  pitoregt0  7536  peano2nnnn  7540  recidpirq  7545  axcaucvglemval  7582  leid  7719  nltled  7754  readdcan  7773  addneintrd  7821  addneintr2d  7822  pncan  7839  subsub2  7861  subsub4  7866  negned  7941  subne0d  7953  subneintrd  7988  subneintr2d  7990  subeq0bd  8008  subdi  8014  gt0add  8201  rimul  8213  rereim  8214  ltmul1a  8219  apreim  8231  apirr  8233  mulap0r  8243  msqge0  8244  mulge0  8247  gt0ap0  8254  ltap  8260  recexaplem2  8274  mulap0bad  8281  mulap0bbd  8282  mul0eqap  8292  divrecap  8309  div0ap  8323  div1  8324  recrecap  8330  divdivdivap  8334  ddcanap  8347  rerecclap  8351  div2negap  8356  diveqap1bd  8456  recgt0  8466  prodgt0  8468  lemul1a  8474  recp1lt1  8515  squeeze0  8520  peano2nn  8590  div4p1lem1div2  8825  arch  8826  peano2z  8942  peano2zm  8944  ztri3or  8949  nn0n0n1ge2  8973  zextle  8994  gtndiv  8998  suprzclex  9001  nn0ind-raph  9020  uzid  9190  uzneg  9194  uztric  9197  uz11  9198  eluzp1l  9200  qdivcl  9285  irrmul  9289  rpnegap  9323  ledivge1le  9360  nn0ledivnn  9395  ltpnf  9408  mnflt  9410  pnfge  9416  mnfle  9419  xrlttr  9422  xrltso  9423  xrlttri3  9424  xrleid  9427  xaddass2  9494  xltadd1  9500  xlt2add  9504  xleaddadd  9511  iccf1o  9628  fztri3or  9660  fznlem  9662  fzn  9663  fzsplit2  9671  fznatpl1  9697  uzsplit  9713  fseq1p1m1  9715  fzm1  9721  fznn0sub2  9746  difelfznle  9753  1fv  9757  fzodcel  9770  fzospliti  9794  fzouzsplit  9797  eluzgtdifelfzo  9815  exfzdc  9858  subfzo0  9860  exbtwnz  9869  qbtwnrelemcalc  9874  flqlelt  9890  qfraclt1  9894  qfracge0  9895  flqltnz  9901  btwnzge0  9914  flhalf  9916  ceiqle  9927  intfracq  9934  mulqmod0  9944  modqge0  9946  modqlt  9947  modqid  9963  modqid0  9964  m1modge3gt1  9985  modqltm1p1mod  9990  q2txmodxeq0  9998  modaddmodlo  10002  modsumfzodifsn  10010  addmodlteq  10012  frecuzrdgtcl  10026  frecuzrdgtclt  10035  uzennn  10050  uzsinds  10056  seqf  10075  seqf2  10078  monoord2  10091  iseqf1olemqk  10108  iseqf1olemjpcl  10109  iseqf1olemqpcl  10110  seq3f1olemqsumkj  10112  seq3f1olemqsum  10114  seq3f1olemstep  10115  seq3f1oleml  10117  ser3le  10132  exp3vallem  10135  exp3val  10136  expp1  10141  expcllem  10145  ltexp2a  10186  leexp2a  10187  faclbnd  10328  faclbnd2  10329  faclbnd3  10330  bcval5  10350  bcpasc  10353  hashennn  10367  fihasheqf1oi  10375  hashsng  10385  fihashfn  10387  hashun  10392  fihashss  10403  fihashssdif  10405  hashfz  10408  hashxp  10413  fimaxq  10414  zfz1isolem1  10424  seq3coll  10426  shftfn  10437  cjth  10459  cjmulrcl  10500  reim0bd  10557  rerebd  10558  cjrebd  10559  caucvgre  10593  cvg1nlemcxze  10594  cvg1nlemcau  10596  cvg1nlemres  10597  recvguniq  10607  resqrexlemover  10622  resqrexlemdec  10623  resqrexlemgt0  10632  resqrexlemoverl  10633  resqrexlemglsq  10634  rersqrtthlem  10642  sqrtgt0  10646  leabs  10686  absexpzap  10692  absle  10701  recvalap  10709  abstri  10716  abs2dif  10718  amgm2  10730  absne0d  10799  maxleim  10817  maxabslemab  10818  maxabslemlub  10819  maxltsup  10830  zmaxcl  10835  fimaxre2  10837  minmax  10840  rpmincl  10848  bdtrilem  10849  bdtri  10850  xrmaxleim  10852  xrmaxiflemcom  10857  xrmaxltsup  10866  xrmaxadd  10869  xrminmax  10873  xrminrpcl  10882  climconst  10898  climuni  10901  2clim  10909  climcn1  10916  climcn2  10917  reccn2ap  10921  climge0  10933  climle  10942  climsqz  10943  climsqz2  10944  serf0  10960  summodclem3  10988  summodclem2a  10989  fsumcl2lem  11006  sumpr  11021  sumtp  11022  fsum0diaglem  11048  mptfzshft  11050  fsumle  11071  fsumlt  11072  divcnv  11105  trireciplem  11108  expcnvap0  11110  expcnv  11112  explecnv  11113  geosergap  11114  cvgratnnlembern  11131  cvgratnnlemabsle  11135  cvgratnnlemsumlt  11136  cvgratz  11140  cvgratgt0  11141  mertenslemi1  11143  mertenslem2  11144  mertensabs  11145  eftcl  11158  ef0lem  11164  efsub  11185  eftlub  11194  eflegeo  11206  tanval2ap  11218  sinadd  11241  cos2t  11255  cos2tsin  11256  sin01bnd  11262  cos01bnd  11263  eirraplem  11278  dvdsval2  11291  dvdsdc  11296  dvds0lem  11298  zdvdsdc  11309  dvdscmulr  11317  dvdsmulcr  11318  dvdslelemd  11336  divconjdvds  11342  dvdsext  11348  fzm1ndvds  11349  dvdsmod  11355  oexpneg  11369  2tp1odd  11376  mulsucdiv2z  11377  2teven  11379  zeo5  11380  opeo  11389  omeo  11390  nn0ob  11400  divalglemnqt  11412  zsupcllemstep  11433  zsupcl  11435  zssinfcl  11436  infssuzex  11437  infssuzcldc  11439  gcddvds  11447  dvdslegcd  11448  gcdneg  11465  bezoutlemnewy  11477  bezoutlemstep  11478  bezoutlema  11480  bezoutlemb  11481  bezoutlemmo  11487  bezoutlemle  11489  bezoutlemsup  11490  dfgcd3  11491  bezout  11492  dfgcd2  11495  lcmcllem  11541  lcmneg  11548  lcmgcdlem  11551  lcmdvds  11553  lcmid  11554  3lcm2e6woprm  11560  6lcm4e12  11561  ncoprmgcdne1b  11563  mulgcddvds  11568  divgcdcoprmex  11576  cncongr1  11577  cncongr2  11578  isprm2lem  11590  prmind2  11594  dvdsnprmd  11599  prm2orodd  11600  sqnprm  11609  rpexp  11624  sqrt2irrlem  11632  oddpwdclemdc  11643  sqrt2irraplemnn  11649  qnumdencoprm  11663  qeqnumdivden  11664  nn0gcdsq  11670  nn0sqrtelqelz  11676  nonsq  11677  phicl2  11682  phibnd  11685  hashdvds  11689  phiprmpw  11690  phimullem  11693  hashgcdlem  11695  znnen  11703  ennnfonelemk  11705  ennnfonelemkh  11717  ennnfonelemhf1o  11718  ennnfonelemrnh  11721  ennnfonelemfun  11722  ennnfonelemf1  11723  ennnfonelemrn  11724  ennnfonelemnn0  11727  ctinfomlemom  11732  structfung  11758  setsfun  11776  setsfun0  11777  setscom  11781  setsslid  11791  baspartn  11999  eltg3i  12007  tgclb  12016  topbas  12018  2basgeng  12033  topcld  12060  0cld  12063  uncld  12064  neif  12092  elnei  12103  0nei  12117  restbasg  12119  iscnp4  12168  cnpnei  12169  cnclima  12173  cncnp  12180  cnrest2r  12187  cndis  12191  lmff  12199  lmtopcnp  12200  txbas  12208  txopn  12215  txcnp  12221  upxp  12222  txdis1cn  12228  cnmpt11  12233  cnmpt21  12241  psmetge0  12259  xmetge0  12293  xmettpos  12298  xmetrtri  12304  metrtri  12305  xblpnfps  12326  xblpnf  12327  blfps  12337  blf  12338  ssblps  12353  ssbl  12354  blbas  12361  metss2  12426  qtopbas  12444  cncfss  12483  cdivcncfap  12499  expcncf  12504  ellimc3ap  12511  limcimolemlt  12513  limcimo  12514  limcresi  12515  reldvg  12521  dvfgg  12530  dvidlemap  12533  bj-sels  12693  bj-nnelon  12742  pwle2  12779  pwf1oexmid  12780  nninfall  12788  nninfsellemdc  12790  nninfself  12793  refeq  12807  isomninnlem  12809  cvgcmp2nlemabs  12811  trilpolemlt1  12818