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-mp 5  ax-1 6  ax-2 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  701  mpbir2and  939  pm3.12dc  953  mpbir3and  1175  pm5.15dc  1384  eqeltrd  2247  eqnetrd  2364  3netr4d  2373  r19.30dc  2617  sbcne12g  3067  eqsstrd  3183  3sstr4d  3192  eqbrtrd  4011  3brtr4d  4021  snelpwi  4197  prelpwi  4199  pwel  4203  ordelon  4368  onin  4371  elelsuc  4394  suceloni  4485  sucelon  4487  onintonm  4501  omsinds  4606  sosng  4684  relssdv  4703  eqbrrdv  4708  eqrelrdv2  4710  relsnopg  4715  breldmg  4817  elrnmptdv  4865  iss  4937  xpimasn  5059  elxp4  5098  elxp5  5099  iotam  5190  funssres  5240  f0rn0  5392  sefvex  5517  fvun1  5562  eqfnfvd  5596  fvimacnvi  5610  fvimacnv  5611  fvelrn  5627  fmpt3d  5652  fmpt2d  5658  resflem  5660  fmptco  5662  fsn  5668  ftpg  5680  fconst2g  5711  funfvima3  5729  foeqcnvco  5769  f1eqcocnv  5770  fliftfun  5775  fliftfund  5776  fliftval  5779  riota5f  5833  f1ofveu  5841  f1ocnvd  6051  f1opw2  6055  off  6073  offval2  6076  ofrfval2  6077  caofref  6082  caofinvl  6083  elxp6  6148  cnvf1olem  6203  f2ndf  6205  f1od2  6214  tposf12  6248  smores2  6273  tfrlemisucaccv  6304  tfrlemibfn  6307  tfr1onlemsucaccv  6320  tfr1onlembfn  6323  tfrcllemsucaccv  6333  tfrcllembfn  6336  tfrcl  6343  tfri3  6346  frecabcl  6378  nnsucsssuc  6471  ersym  6525  ertr  6528  swoer  6541  erth  6557  riinerm  6586  qliftfund  6596  eroprf  6606  ecopoverg  6614  th3qlem1  6615  elmapssres  6651  mapss  6669  fdiagfn  6670  ixpssmap2g  6705  mapsnf1o  6715  f1dom2g  6734  dom3d  6752  fopwdom  6814  mapxpen  6826  nndomo  6842  dif1en  6857  findcard2  6867  findcard2s  6868  diffisn  6871  fimax2gtrilemstep  6878  fientri3  6892  fiintim  6906  f1dmvrnfibi  6921  sbthlemi6  6939  elfir  6950  fifo  6957  supelti  6979  supsnti  6982  cnvinfex  6995  ordiso2  7012  updjud  7059  djudom  7070  difinfsn  7077  ctssdc  7090  enumctlemm  7091  enumct  7092  enomnilem  7114  fodjuf  7121  ismkvnex  7131  omnimkv  7132  enmkvlem  7137  enwomnilem  7145  nninfdcinf  7147  nninfwlporlem  7149  isnumi  7159  exmidfodomrlemrALT  7180  djudoml  7196  djudomr  7197  cc2lem  7228  cc3  7230  ltsopi  7282  pitri3or  7284  ltdcpi  7285  indpi  7304  enqdc  7323  enqdc1  7324  addcmpblnq  7329  mulcanenq  7347  recrecnq  7356  nqtri3or  7358  ltdcnq  7359  ltsonq  7360  ltaddnq  7369  subhalfnqq  7376  archnqq  7379  prarloclemarch2  7381  enq0tr  7396  nqnq0  7403  addcmpblnq0  7405  mulcanenq0ec  7407  nnnq0lem1  7408  nqpnq0nq  7415  nq0m0r  7418  nq02m  7427  prarloclemlt  7455  prarloclemcalc  7464  addlocpr  7498  nqprl  7513  nqpru  7514  addnqprlemrl  7519  addnqprlemru  7520  prmuloclemcalc  7527  mullocprlem  7532  mulnqprlemrl  7535  mulnqprlemru  7536  1idprl  7552  1idpru  7553  ltaddpr  7559  ltexprlemm  7562  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemdisj  7568  ltexprlemrl  7572  ltexprlemru  7574  addcanprleml  7576  addcanprlemu  7577  addcanprg  7578  prplnqu  7582  recexprlemloc  7593  recexprlem1ssl  7595  recexprlem1ssu  7596  aptiprleml  7601  aptiprlemu  7602  archpr  7605  cauappcvgprlemm  7607  cauappcvgprlemopl  7608  cauappcvgprlemloc  7614  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  cauappcvgprlem1  7621  cauappcvgprlem2  7622  caucvgprlemnkj  7628  caucvgprlemopl  7631  caucvgprlemloc  7637  caucvgprlemladdfu  7639  caucvgprlem2  7642  caucvgprprlemnkltj  7651  caucvgprprlemopl  7659  caucvgprprlemloc  7665  caucvgprprlemexbt  7668  caucvgprprlemaddq  7670  caucvgprprlem2  7672  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemloc  7683  suplocexprlemlub  7686  prsrlem1  7704  0idsr  7729  1idsr  7730  recexgt0sr  7735  archsr  7744  prsradd  7748  caucvgsrlemcau  7755  caucvgsrlembound  7756  caucvgsrlemoffgt1  7761  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  pitonnlem1p1  7808  pitonn  7810  pitoregt0  7811  peano2nnnn  7815  recidpirq  7820  axcaucvglemval  7859  leid  8003  nltled  8040  readdcan  8059  addneintrd  8107  addneintr2d  8108  pncan  8125  subsub2  8147  subsub4  8152  negned  8227  subne0d  8239  subneintrd  8274  subneintr2d  8276  subeq0bd  8298  subdi  8304  gt0add  8492  rimul  8504  rereim  8505  ltmul1a  8510  apreim  8522  apirr  8524  mulap0r  8534  msqge0  8535  mulge0  8538  gt0ap0  8545  ltap  8552  subap0d  8563  recexaplem2  8570  mulap0bad  8577  mulap0bbd  8578  mul0eqap  8588  divrecap  8605  div0ap  8619  div1  8620  recrecap  8626  divdivdivap  8630  ddcanap  8643  rerecclap  8647  div2negap  8652  diveqap1bd  8753  recgt0  8766  prodgt0  8768  lemul1a  8774  recp1lt1  8815  squeeze0  8820  peano2nn  8890  div4p1lem1div2  9131  arch  9132  peano2z  9248  peano2zm  9250  ztri3or  9255  nn0n0n1ge2  9282  zextle  9303  gtndiv  9307  suprzclex  9310  nn0ind-raph  9329  uzid  9501  uzneg  9505  uztric  9508  uz11  9509  eluzp1l  9511  qdivcl  9602  irrmul  9606  rpnegap  9643  negelrpd  9645  ledivge1le  9683  mul2lt0rlt0  9716  mul2lt0rgt0  9717  nn0ledivnn  9724  ltpnf  9737  mnflt  9740  pnfge  9746  mnfle  9749  xrlttr  9752  xrltso  9753  xrlttri3  9754  xrleid  9757  xaddass2  9827  xltadd1  9833  xlt2add  9837  xleaddadd  9844  iccf1o  9961  fztri3or  9995  fznlem  9997  fzn  9998  fzsplit2  10006  fznatpl1  10032  uzsplit  10048  fseq1p1m1  10050  fzm1  10056  fznn0sub2  10084  difelfznle  10091  1fv  10095  fzodcel  10108  fzospliti  10132  fzouzsplit  10135  eluzgtdifelfzo  10153  exfzdc  10196  subfzo0  10198  exbtwnz  10207  qbtwnrelemcalc  10212  flqlelt  10232  qfraclt1  10236  qfracge0  10237  flqltnz  10243  btwnzge0  10256  flhalf  10258  ceiqle  10269  intfracq  10276  mulqmod0  10286  modqge0  10288  modqlt  10289  modqid  10305  modqid0  10306  m1modge3gt1  10327  modqltm1p1mod  10332  q2txmodxeq0  10340  modaddmodlo  10344  modsumfzodifsn  10352  addmodlteq  10354  frecuzrdgtcl  10368  frecuzrdgtclt  10377  uzennn  10392  uzsinds  10398  seqf  10417  seqf2  10420  monoord2  10433  iseqf1olemqk  10450  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  seq3f1olemqsumkj  10454  seq3f1olemqsum  10456  seq3f1olemstep  10457  seq3f1oleml  10459  ser3le  10474  exp3vallem  10477  exp3val  10478  expp1  10483  expcllem  10487  ltexp2a  10528  leexp2a  10529  nn0ltexp2  10644  faclbnd  10675  faclbnd2  10676  faclbnd3  10677  bcval5  10697  bcpasc  10700  hashennn  10714  fihasheqf1oi  10722  hashsng  10733  fihashfn  10735  hashun  10740  fihashss  10751  fihashssdif  10753  hashfz  10756  hashxp  10761  fimaxq  10762  zfz1isolem1  10775  seq3coll  10777  shftfn  10788  cjth  10810  cjmulrcl  10851  reim0bd  10908  rerebd  10909  cjrebd  10910  caucvgre  10945  cvg1nlemcxze  10946  cvg1nlemcau  10948  cvg1nlemres  10949  recvguniq  10959  resqrexlemover  10974  resqrexlemdec  10975  resqrexlemgt0  10984  resqrexlemoverl  10985  resqrexlemglsq  10986  rersqrtthlem  10994  sqrtgt0  10998  leabs  11038  absexpzap  11044  absle  11053  recvalap  11061  abstri  11068  abs2dif  11070  amgm2  11082  absne0d  11151  maxleim  11169  maxabslemab  11170  maxabslemlub  11171  maxltsup  11182  zmaxcl  11188  fimaxre2  11190  minmax  11193  rpmincl  11201  bdtrilem  11202  bdtri  11203  xrmaxleim  11207  xrmaxiflemcom  11212  xrmaxltsup  11221  xrmaxadd  11224  xrminmax  11228  xrminrpcl  11237  climconst  11253  climuni  11256  2clim  11264  climcn1  11271  climcn2  11272  reccn2ap  11276  climge0  11288  climle  11297  climsqz  11298  climsqz2  11299  serf0  11315  summodclem3  11343  summodclem2a  11344  fsumcl2lem  11361  sumpr  11376  sumtp  11377  fsum0diaglem  11403  mptfzshft  11405  fsumle  11426  fsumlt  11427  divcnv  11460  trireciplem  11463  expcnvap0  11465  expcnv  11467  explecnv  11468  geosergap  11469  cvgratnnlembern  11486  cvgratnnlemabsle  11490  cvgratnnlemsumlt  11491  cvgratz  11495  cvgratgt0  11496  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  clim2divap  11503  prodmodclem3  11538  prodmodclem2a  11539  fprodseq  11546  fprodmul  11554  fprodfac  11578  fprodconst  11583  fprodap0  11584  fprodap0f  11599  fprodle  11603  eftcl  11617  ef0lem  11623  efsub  11644  eftlub  11653  eflegeo  11664  tanval2ap  11676  sinadd  11699  cos2t  11713  cos2tsin  11714  sin01bnd  11720  cos01bnd  11721  eirraplem  11739  dvdsval2  11752  dvdsdc  11760  dvds0lem  11763  zdvdsdc  11774  dvdscmulr  11782  dvdsmulcr  11783  dvdslelemd  11803  divconjdvds  11809  dvdsext  11815  fzm1ndvds  11816  dvdsmod  11822  oexpneg  11836  2tp1odd  11843  mulsucdiv2z  11844  2teven  11846  zeo5  11847  opeo  11856  omeo  11857  nn0ob  11867  divalglemnqt  11879  zsupcllemstep  11900  zsupcl  11902  zssinfcl  11903  infssuzex  11904  infssuzcldc  11906  suprzubdc  11907  nninfdcex  11908  gcddvds  11918  dvdslegcd  11919  gcdneg  11937  bezoutlemnewy  11951  bezoutlemstep  11952  bezoutlema  11954  bezoutlemb  11955  bezoutlemmo  11961  bezoutlemle  11963  bezoutlemsup  11964  dfgcd3  11965  bezout  11966  dfgcd2  11969  uzwodc  11992  lcmcllem  12021  lcmneg  12028  lcmgcdlem  12031  lcmdvds  12033  lcmid  12034  3lcm2e6woprm  12040  6lcm4e12  12041  ncoprmgcdne1b  12043  mulgcddvds  12048  divgcdcoprmex  12056  cncongr1  12057  cncongr2  12058  isprm2lem  12070  prmind2  12074  dvdsnprmd  12079  prm2orodd  12080  sqnprm  12090  isprm5lem  12095  rpexp  12107  sqrt2irrlem  12115  oddpwdclemdc  12127  sqrt2irraplemnn  12133  qnumdencoprm  12147  qeqnumdivden  12148  nn0gcdsq  12154  nn0sqrtelqelz  12160  nonsq  12161  phicl2  12168  phibnd  12171  hashdvds  12175  phiprmpw  12176  phimullem  12179  eulerthlemrprm  12183  eulerthlema  12184  eulerthlemth  12186  prmdiveq  12190  hashgcdlem  12192  odzdvds  12199  modprminv  12203  nnnn0modprm0  12209  modprmn0modprm0  12210  pythagtriplem10  12223  pythagtriplem19  12236  pythagtrip  12237  pcpre1  12246  pcpremul  12247  pceu  12249  pcmul  12255  pcdiv  12256  pcqmul  12257  pcqdiv  12261  pcexp  12263  pcdvdsb  12273  pcidlem  12276  pcdvdstr  12280  pcgcd1  12281  pc2dvds  12283  pcprmpw2  12286  difsqpwdvds  12291  pcaddlem  12292  pcadd  12293  pcmpt  12295  pcmptdvds  12297  pcprod  12298  fldivp1  12300  pcfaclem  12301  pcfac  12302  pcbc  12303  qexpz  12304  pockthlem  12308  pockthg  12309  1arithlem4  12318  1arith  12319  1arith2  12320  4sqlem6  12335  4sqlem8  12337  4sqlem9  12338  4sqlem10  12339  znnen  12353  ennnfonelemk  12355  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemrnh  12371  ennnfonelemfun  12372  ennnfonelemf1  12373  ennnfonelemrn  12374  ennnfonelemnn0  12377  ctinfomlemom  12382  ctiunctlemudc  12392  unct  12397  omctfn  12398  ssnnctlemct  12401  nninfdclemp1  12405  nninfdc  12408  structfung  12433  setsfun  12451  setsfun0  12452  setscom  12456  setsslid  12466  mgmsscl  12615  plusffng  12619  mgmplusf  12620  mgm0  12623  mgm1  12624  opifismgmdc  12625  sgrp1  12651  mndpfo  12674  mndfo  12675  mnd1  12679  0subm  12702  mhmima  12706  grpinvfng  12747  isgrpinv  12756  grpinvid  12760  grpinvf1o  12769  baspartn  12842  eltg3i  12850  tgclb  12859  topbas  12861  2basgeng  12876  topcld  12903  0cld  12906  uncld  12907  neif  12935  elnei  12946  0nei  12960  restbasg  12962  iscnp4  13012  cnpnei  13013  cnclima  13017  cncnp  13024  cnrest2r  13031  cndis  13035  lmff  13043  lmtopcnp  13044  txbas  13052  txopn  13059  txcnp  13065  upxp  13066  txdis1cn  13072  cnmpt11  13077  cnmpt21  13085  psmetge0  13125  xmetge0  13159  xmettpos  13164  xmetrtri  13170  metrtri  13171  xblpnfps  13192  xblpnf  13193  blfps  13203  blf  13204  ssblps  13219  ssbl  13220  blbas  13227  metss2  13292  xmettxlem  13303  xmettx  13304  qtopbas  13316  divcnap  13349  cncfss  13364  cdivcncfap  13381  expcncf  13386  cnopnap  13388  dedekindeulemuub  13389  dedekindeulemlu  13393  dedekindeu  13395  suplociccex  13397  dedekindicclemuub  13398  dedekindicclemlu  13402  dedekindicclemicc  13404  ivthinclemlopn  13408  ivthinclemuopn  13410  ivthinc  13415  ellimc3apf  13423  limcimolemlt  13427  limcimo  13428  limcresi  13429  cnplimclemle  13431  reldvg  13442  dvfgg  13451  dvidlemap  13454  dvcjbr  13466  dvcj  13467  dvrecap  13471  dveflem  13481  dvef  13482  reeff1oleme  13487  pilem3  13498  sinq34lt0t  13546  cosq14gt0  13547  coseq0q4123  13549  tangtx  13553  sincosq1eq  13554  cosordlem  13564  logdivlti  13596  relogbval  13663  relogbzcl  13664  nnlogbexp  13671  logbgcd1irr  13679  logbgcd1irraplemexp  13680  logbgcd1irraplemap  13681  zabsle1  13694  lgslem1  13695  lgsval  13699  lgsfvalg  13700  lgsfcl2  13701  lgsval2lem  13705  lgscl1  13718  lgsmod  13721  lgsdir2lem5  13727  lgsdir2  13728  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  2sqlem3  13747  2sqlem8  13753  2sqlem10  13755  fnmptd  13839  bj-sels  13949  bj-nnelon  13994  pwle2  14031  pwf1oexmid  14032  pw1nct  14036  nninfall  14042  nninfsellemdc  14043  nninfself  14046  refeq  14060  isomninnlem  14062  cvgcmp2nlemabs  14064  trilpolemlt1  14073  trirec0  14076  apdifflemf  14078  apdifflemr  14079  apdiff  14080  iswomninnlem  14081  iswomni0  14083  ismkvnnlem  14084  reap0  14090