Theorem mpbird 167

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbiri  168  pm5.19  708  pm4.55dc  941  mpbir2and  947  pm3.12dc  961  mpbir3and  1183  pm5.15dc  1409  eqeltrd  2283  eqnetrd  2401  3netr4d  2410  r19.30dc  2654  raleqtrrdv  2713  rexeqtrrdv  2714  sbcne12g  3115  eqsstrd  3233  3sstr4d  3242  eqbrtrd  4073  3brtr4d  4083  snelpwi  4264  prelpwi  4266  pwel  4270  ordelon  4438  onin  4441  elelsuc  4464  onsuc  4557  onsucb  4559  onintonm  4573  omsinds  4678  sosng  4756  relssdv  4775  eqbrrdv  4780  eqrelrdv2  4782  relsnopg  4787  breldmg  4893  elrnmptdv  4941  iss  5014  xpimasn  5140  elxp4  5179  elxp5  5180  iotam  5272  funssres  5322  f0rn0  5482  fimadmfo  5519  sefvex  5610  fvun1  5658  eqfnfvd  5693  fvimacnvi  5707  fvimacnv  5708  fvelrn  5724  fmpt3d  5749  fmpt2d  5755  resflem  5757  fmptco  5759  fsn  5765  funopsn  5775  ftpg  5781  fconst2g  5812  funfvima3  5831  elabrexg  5840  foeqcnvco  5872  f1eqcocnv  5873  fliftfun  5878  fliftfund  5879  fliftval  5882  riota5f  5937  f1ofveu  5945  f1ocnvd  6161  f1opw2  6165  off  6184  offval2  6187  ofrfval2  6188  offveq  6192  caofref  6196  caofinvl  6197  elxp6  6268  cnvf1olem  6323  f2ndf  6325  f1od2  6334  tposf12  6368  smores2  6393  tfrlemisucaccv  6424  tfrlemibfn  6427  tfr1onlemsucaccv  6440  tfr1onlembfn  6443  tfrcllemsucaccv  6453  tfrcllembfn  6456  tfrcl  6463  tfri3  6466  frecabcl  6498  nnsucsssuc  6591  ersym  6645  ertr  6648  swoer  6661  erth  6679  riinerm  6708  qliftfund  6718  eroprf  6728  ecopoverg  6736  th3qlem1  6737  elmapssres  6773  mapss  6791  fdiagfn  6792  ixpssmap2g  6827  mapsnf1o  6837  f1oen4g  6856  f1dom4g  6857  f1dom2g  6860  dom3d  6878  en2prd  6923  pw2f1odclem  6946  fopwdom  6948  mapxpen  6960  nndomo  6976  dif1en  6991  findcard2  7001  findcard2s  7002  diffisn  7005  fimax2gtrilemstep  7012  fientri3  7027  tpfidceq  7042  fiintim  7043  opabfi  7050  f1dmvrnfibi  7061  sbthlemi6  7079  elfir  7090  fifo  7097  supelti  7119  supsnti  7122  cnvinfex  7135  ordiso2  7152  updjud  7199  djudom  7210  difinfsn  7217  ctssdc  7230  enumctlemm  7231  enumct  7232  nninfninc  7240  enomnilem  7255  fodjuf  7262  ismkvnex  7272  omnimkv  7273  enmkvlem  7278  enwomnilem  7286  nninfdcinf  7288  nninfwlporlem  7290  isnumi  7304  exmidfodomrlemrALT  7327  finacn  7332  djudoml  7347  djudomr  7348  netap  7386  2omotaplemap  7389  2omotaplemst  7390  exmidapne  7392  cc2lem  7398  cc3  7400  ltsopi  7453  pitri3or  7455  ltdcpi  7456  indpi  7475  enqdc  7494  enqdc1  7495  addcmpblnq  7500  mulcanenq  7518  recrecnq  7527  nqtri3or  7529  ltdcnq  7530  ltsonq  7531  ltaddnq  7540  subhalfnqq  7547  archnqq  7550  prarloclemarch2  7552  enq0tr  7567  nqnq0  7574  addcmpblnq0  7576  mulcanenq0ec  7578  nnnq0lem1  7579  nqpnq0nq  7586  nq0m0r  7589  nq02m  7598  prarloclemlt  7626  prarloclemcalc  7635  addlocpr  7669  nqprl  7684  nqpru  7685  addnqprlemrl  7690  addnqprlemru  7691  prmuloclemcalc  7698  mullocprlem  7703  mulnqprlemrl  7706  mulnqprlemru  7707  1idprl  7723  1idpru  7724  ltaddpr  7730  ltexprlemm  7733  ltexprlemopl  7734  ltexprlemopu  7736  ltexprlemdisj  7739  ltexprlemrl  7743  ltexprlemru  7745  addcanprleml  7747  addcanprlemu  7748  addcanprg  7749  prplnqu  7753  recexprlemloc  7764  recexprlem1ssl  7766  recexprlem1ssu  7767  aptiprleml  7772  aptiprlemu  7773  archpr  7776  cauappcvgprlemm  7778  cauappcvgprlemopl  7779  cauappcvgprlemloc  7785  cauappcvgprlemladdfu  7787  cauappcvgprlemladdfl  7788  cauappcvgprlem1  7792  cauappcvgprlem2  7793  caucvgprlemnkj  7799  caucvgprlemopl  7802  caucvgprlemloc  7808  caucvgprlemladdfu  7810  caucvgprlem2  7813  caucvgprprlemnkltj  7822  caucvgprprlemopl  7830  caucvgprprlemloc  7836  caucvgprprlemexbt  7839  caucvgprprlemaddq  7841  caucvgprprlem2  7843  suplocexprlemmu  7851  suplocexprlemru  7852  suplocexprlemloc  7854  suplocexprlemlub  7857  prsrlem1  7875  0idsr  7900  1idsr  7901  recexgt0sr  7906  archsr  7915  prsradd  7919  caucvgsrlemcau  7926  caucvgsrlembound  7927  caucvgsrlemoffgt1  7932  suplocsrlemb  7939  suplocsrlempr  7940  suplocsrlem  7941  pitonnlem1p1  7979  pitonn  7981  pitoregt0  7982  peano2nnnn  7986  recidpirq  7991  axcaucvglemval  8030  leid  8176  nltled  8213  readdcan  8232  addneintrd  8280  addneintr2d  8281  pncan  8298  subsub2  8320  subsub4  8325  negned  8400  subne0d  8412  subneintrd  8447  subneintr2d  8449  subeq0bd  8471  subdi  8477  gt0add  8666  rimul  8678  rereim  8679  ltmul1a  8684  apreim  8696  apirr  8698  mulap0r  8708  msqge0  8709  mulge0  8712  gt0ap0  8719  ltap  8726  subap0d  8737  recexaplem2  8745  mulap0bad  8752  mulap0bbd  8753  mul0eqap  8763  divrecap  8781  div0ap  8795  div1  8796  recrecap  8802  divdivdivap  8806  ddcanap  8819  rerecclap  8823  div2negap  8828  diveqap1bd  8929  recgt0  8943  prodgt0  8945  lemul1a  8951  recp1lt1  8992  squeeze0  8997  peano2nn  9068  div4p1lem1div2  9311  arch  9312  peano2z  9428  peano2zm  9430  ztri3or  9435  nn0n0n1ge2  9463  zextle  9484  gtndiv  9488  suprzclex  9491  nn0ind-raph  9510  uzid  9682  uzneg  9687  uztric  9690  uz11  9691  eluzp1l  9693  qdivcl  9784  irrmul  9788  irrmulap  9789  rpnegap  9828  negelrpd  9830  ledivge1le  9868  mul2lt0rlt0  9901  mul2lt0rgt0  9902  nn0ledivnn  9909  ltpnf  9922  mnflt  9925  pnfge  9931  mnfle  9934  xrlttr  9937  xrltso  9938  xrlttri3  9939  xrleid  9942  xaddass2  10012  xltadd1  10018  xlt2add  10022  xleaddadd  10029  iccf1o  10146  fztri3or  10181  fznlem  10183  fzn  10184  fzsplit2  10192  fznatpl1  10218  uzsplit  10234  fseq1p1m1  10236  fzm1  10242  fznn0sub2  10270  difelfznle  10277  1fv  10281  fzodcel  10295  fzospliti  10320  fzouzsplit  10323  eluzgtdifelfzo  10348  exfzdc  10391  subfzo0  10393  zsupcllemstep  10394  zsupcl  10396  zssinfcl  10397  infssuzex  10398  infssuzcldc  10400  suprzubdc  10401  nninfdcex  10402  qdcle  10411  exbtwnz  10415  qbtwnrelemcalc  10420  flqlelt  10441  qfraclt1  10445  qfracge0  10446  flqltnz  10452  btwnzge0  10465  flhalf  10467  fldiv4lem1div2uz2  10471  ceiqle  10480  intfracq  10487  mulqmod0  10497  modqge0  10499  modqlt  10500  modqid  10516  modqid0  10517  m1modge3gt1  10538  modqltm1p1mod  10543  q2txmodxeq0  10551  modaddmodlo  10555  modsumfzodifsn  10563  addmodlteq  10565  frecuzrdgtcl  10579  frecuzrdgtclt  10588  uzennn  10603  uzsinds  10611  seqf  10631  seqf2  10635  monoord2  10653  iseqf1olemqk  10674  iseqf1olemjpcl  10675  iseqf1olemqpcl  10676  seq3f1olemqsumkj  10678  seq3f1olemqsum  10680  seq3f1olemstep  10681  seq3f1oleml  10683  seqf1oglem1  10686  ser3le  10704  exp3vallem  10707  exp3val  10708  expp1  10713  expcllem  10717  ltexp2a  10758  leexp2a  10759  nn0ltexp2  10876  faclbnd  10908  faclbnd2  10909  faclbnd3  10910  bcval5  10930  bcpasc  10933  hashennn  10947  fihasheqf1oi  10954  hashsng  10965  fihashfn  10967  hashun  10972  fihashss  10983  fihashssdif  10985  hashfz  10988  hashxp  10993  fimaxq  10994  zfz1isolem1  11007  seq3coll  11009  hashdmprop2dom  11011  wrdf  11022  wrdlenge2n0  11051  fstwrdne0  11055  wrdred1hash  11059  ccatvalfn  11080  ccatsymb  11081  ccatlid  11085  ccatrid  11086  ccatrn  11088  eqs1  11105  ccats1val2  11115  fzowrddc  11123  swrdlen  11128  swrdnd  11135  swrd0g  11136  swrdfv2  11139  swrdwrdsymbg  11140  pfxn0  11164  pfxwrdsymbg  11166  pfxsuff1eqwrdeq  11175  swrdswrd  11181  ccats1pfxeq  11190  ccats1pfxeqrex  11191  wrdind  11198  wrd2ind  11199  shftfn  11210  cjth  11232  cjmulrcl  11273  reim0bd  11330  rerebd  11331  cjrebd  11332  caucvgre  11367  cvg1nlemcxze  11368  cvg1nlemcau  11370  cvg1nlemres  11371  recvguniq  11381  resqrexlemover  11396  resqrexlemdec  11397  resqrexlemgt0  11406  resqrexlemoverl  11407  resqrexlemglsq  11408  rersqrtthlem  11416  sqrtgt0  11420  leabs  11460  absexpzap  11466  absle  11475  recvalap  11483  abstri  11490  abs2dif  11492  amgm2  11504  absne0d  11573  maxleim  11591  maxabslemab  11592  maxabslemlub  11593  maxltsup  11604  zmaxcl  11610  fimaxre2  11613  minmax  11616  rpmincl  11624  bdtrilem  11625  bdtri  11626  xrmaxleim  11630  xrmaxiflemcom  11635  xrmaxltsup  11644  xrmaxadd  11647  xrminmax  11651  xrminrpcl  11660  climconst  11676  climuni  11679  2clim  11687  climcn1  11694  climcn2  11695  reccn2ap  11699  climge0  11711  climle  11720  climsqz  11721  climsqz2  11722  serf0  11738  summodclem3  11766  summodclem2a  11767  fsumcl2lem  11784  sumpr  11799  sumtp  11800  fsum0diaglem  11826  mptfzshft  11828  fsumle  11849  fsumlt  11850  divcnv  11883  trireciplem  11886  expcnvap0  11888  expcnv  11890  explecnv  11891  geosergap  11892  cvgratnnlembern  11909  cvgratnnlemabsle  11913  cvgratnnlemsumlt  11914  cvgratz  11918  cvgratgt0  11919  mertenslemi1  11921  mertenslem2  11922  mertensabs  11923  clim2divap  11926  prodmodclem3  11961  prodmodclem2a  11962  fprodseq  11969  fprodmul  11977  fprodfac  12001  fprodconst  12006  fprodap0  12007  fprodap0f  12022  fprodle  12026  eftcl  12040  ef0lem  12046  efsub  12067  eftlub  12076  eflegeo  12087  tanval2ap  12099  sinadd  12122  cos2t  12136  cos2tsin  12137  sin01bnd  12143  cos01bnd  12144  eirraplem  12163  dvdsval2  12176  dvdsdc  12184  dvds0lem  12187  zdvdsdc  12198  dvdscmulr  12206  dvdsmulcr  12207  fsumdvds  12228  dvdslelemd  12229  divconjdvds  12235  dvdsext  12241  fzm1ndvds  12242  dvdsmod  12248  3dvds  12250  oexpneg  12263  2tp1odd  12270  mulsucdiv2z  12271  2teven  12273  zeo5  12274  opeo  12283  omeo  12284  nn0ob  12294  divalglemnqt  12306  bitsdc  12333  bits0o  12336  bitsfzolem  12340  bitsfzo  12341  bitsmod  12342  bitscmp  12344  bitsinv1lem  12347  gcddvds  12359  dvdslegcd  12360  gcdneg  12378  bezoutlemnewy  12392  bezoutlemstep  12393  bezoutlema  12395  bezoutlemb  12396  bezoutlemmo  12402  bezoutlemle  12404  bezoutlemsup  12405  dfgcd3  12406  bezout  12407  dfgcd2  12410  uzwodc  12433  lcmcllem  12464  lcmneg  12471  lcmgcdlem  12474  lcmdvds  12476  lcmid  12477  3lcm2e6woprm  12483  6lcm4e12  12484  ncoprmgcdne1b  12486  mulgcddvds  12491  divgcdcoprmex  12499  cncongr1  12500  cncongr2  12501  isprm2lem  12513  prmind2  12517  dvdsnprmd  12522  prm2orodd  12523  sqnprm  12533  isprm5lem  12538  rpexp  12550  sqrt2irrlem  12558  oddpwdclemdc  12570  sqrt2irraplemnn  12576  qnumdencoprm  12590  qeqnumdivden  12591  nn0gcdsq  12597  nn0sqrtelqelz  12603  nonsq  12604  phicl2  12611  phibnd  12614  hashdvds  12618  phiprmpw  12619  phimullem  12622  eulerthlemrprm  12626  eulerthlema  12627  eulerthlemth  12629  prmdiveq  12633  hashgcdlem  12635  odzdvds  12643  modprminv  12647  nnnn0modprm0  12653  modprmn0modprm0  12654  pythagtriplem10  12667  pythagtriplem19  12680  pythagtrip  12681  pcpre1  12690  pcpremul  12691  pceu  12693  pcmul  12699  pcdiv  12700  pcqmul  12701  pcqdiv  12705  pcexp  12707  pcdvdsb  12718  pcidlem  12721  pcdvdstr  12725  pcgcd1  12726  pc2dvds  12728  pcprmpw2  12731  difsqpwdvds  12736  pcaddlem  12737  pcadd  12738  pcadd2  12739  pcmpt  12741  pcmptdvds  12743  pcprod  12744  fldivp1  12746  pcfaclem  12747  pcfac  12748  pcbc  12749  qexpz  12750  pockthlem  12754  pockthg  12755  1arithlem4  12764  1arith  12765  1arith2  12766  4sqlem6  12781  4sqlem8  12783  4sqlem9  12784  4sqlem10  12785  4sqexercise1  12796  4sqexercise2  12797  4sqlemsdc  12798  4sqlem11  12799  4sqlem12  12800  4sqlem15  12803  4sqlem16  12804  4sqlem17  12805  znnen  12844  ennnfonelemk  12846  ennnfonelemkh  12858  ennnfonelemhf1o  12859  ennnfonelemrnh  12862  ennnfonelemfun  12863  ennnfonelemf1  12864  ennnfonelemrn  12865  ennnfonelemnn0  12868  ctinfomlemom  12873  ctiunctlemudc  12883  unct  12888  omctfn  12889  ssnnctlemct  12892  nninfdclemp1  12896  nninfdc  12899  structfung  12924  setsfun  12942  setsfun0  12943  setscom  12947  strslfv3  12953  setsslid  12958  pwsdiagel  13204  pwssnf1o  13205  imasaddfnlemg  13221  imasaddvallemg  13222  mgmsscl  13268  plusffng  13272  mgmplusf  13273  mgm0  13276  mgm1  13277  opifismgmdc  13278  gsumfzval  13298  gsumprval  13306  sgrp1  13318  issgrpd  13319  prdsplusgsgrpcl  13321  mndpfo  13345  mndfo  13346  prdsplusgcl  13353  prdsidlem  13354  mnd1  13362  0subm  13391  mhmima  13398  grpinvfng  13451  isgrpinv  13461  grpinvid  13467  grpinvf1o  13477  grpinvadd  13485  grpsubf  13486  grpsubsub4  13500  grplactcnv  13509  grp1  13513  grp1inv  13514  prdsinvlem  13515  prdsinvgd  13517  qusgrp2  13524  mulgfng  13535  subginv  13592  resgrpisgrp  13606  subgintm  13609  0subg  13610  0nsg  13625  qusinv  13647  ghminv  13661  ghmrn  13668  ghmeql  13678  ghmnsgima  13679  kerf1ghm  13685  conjnmz  13690  rngass  13776  rngmneg1  13784  rngmneg2  13785  qusrng  13795  srgideu  13809  srgidmlem  13815  srgpcomp  13827  srg1expzeq1  13832  ringcl  13850  ringideu  13854  ringidmlem  13859  ringnegl  13888  ringnegr  13889  ring1  13896  qusring2  13903  opprringbg  13917  dvdsrd  13931  dvdsr01  13941  isunitd  13943  unitinvcl  13960  unitinvinv  13961  unitnegcl  13967  rhmmul  14001  rhmf1o  14005  nzrunit  14025  lringuplu  14033  subrngintm  14049  subrgsubm  14071  subrgintm  14080  aprsym  14121  scaffng  14146  lmodscaf  14147  lsssn0  14207  lss1d  14220  lssintclm  14221  lspval  14227  lspcl  14228  lspsnid  14244  lspprid1  14248  lspsn  14253  sraval  14274  rspcl  14328  rspssid  14329  rspssp  14331  rnglidlmmgm  14333  rnglidlmsgrp  14334  cnfldneg  14410  zringinvg  14441  expghmap  14444  znzrhfo  14485  znf1o  14488  znhash  14493  znidomb  14495  znrrg  14497  psrbagfi  14510  psraddcl  14517  psr0cl  14518  psrnegcl  14520  psrneg  14524  psr1clfi  14525  mplsubgfilemm  14535  mplsubgfilemcl  14536  baspartn  14597  eltg3i  14603  tgclb  14612  topbas  14614  2basgeng  14629  topcld  14656  0cld  14659  uncld  14660  neif  14688  elnei  14699  0nei  14713  restbasg  14715  iscnp4  14765  cnpnei  14766  cnclima  14770  cncnp  14777  cnrest2r  14784  cndis  14788  lmff  14796  lmtopcnp  14797  txbas  14805  txopn  14812  txcnp  14818  upxp  14819  txdis1cn  14825  cnmpt11  14830  cnmpt21  14838  psmetge0  14878  xmetge0  14912  xmettpos  14917  xmetrtri  14923  metrtri  14924  xblpnfps  14945  xblpnf  14946  blfps  14956  blf  14957  ssblps  14972  ssbl  14973  blbas  14980  metss2  15045  xmettxlem  15056  xmettx  15057  qtopbas  15069  divcnap  15112  cncfss  15130  cdivcncfap  15151  expcncf  15156  cnopnap  15158  maxcncf  15162  mincncf  15163  dedekindeulemuub  15164  dedekindeulemlu  15168  dedekindeu  15170  suplociccex  15172  dedekindicclemuub  15173  dedekindicclemlu  15177  dedekindicclemicc  15179  ivthinclemlopn  15183  ivthinclemuopn  15185  ivthinc  15190  ivthreinc  15192  hoverlt1  15196  ellimc3apf  15207  limcimolemlt  15211  limcimo  15212  limcresi  15213  cnplimclemle  15215  reldvg  15226  dvfgg  15235  dvidlemap  15238  dvidrelem  15239  dvidsslem  15240  dvcjbr  15255  dvcj  15256  dvrecap  15260  dveflem  15273  dvef  15274  elply2  15282  elplyr  15287  plycj  15308  plyreres  15311  reeff1oleme  15319  pilem3  15330  sinq34lt0t  15378  cosq14gt0  15379  coseq0q4123  15381  tangtx  15385  sincosq1eq  15386  cosordlem  15396  logdivlti  15428  relogbval  15498  relogbzcl  15499  nnlogbexp  15506  logbgcd1irr  15514  logbgcd1irraplemexp  15515  logbgcd1irraplemap  15516  wilthlem1  15527  mpodvdsmulf1o  15537  mersenne  15544  perfectlem2  15547  perfect  15548  zabsle1  15551  lgslem1  15552  lgsval  15556  lgsfvalg  15557  lgsfcl2  15558  lgsval2lem  15562  lgscl1  15575  lgsmod  15578  lgsdir2lem5  15584  lgsdir2  15585  lgsdilem2  15588  lgsdi  15589  lgsne0  15590  gausslemma2dlem0c  15603  gausslemma2dlem0h  15608  gausslemma2dlem1a  15610  gausslemma2dlem1f1o  15612  gausslemma2dlem3  15615  lgseisenlem1  15622  lgseisenlem2  15623  lgseisenlem3  15624  lgseisenlem4  15625  lgseisen  15626  lgsquadlem1  15629  lgsquadlem2  15630  lgsquadlem3  15631  lgsquad3  15636  2lgslem3b1  15650  2lgslem3c1  15651  2lgs  15656  2lgsoddprmlem2  15658  2lgsoddprm  15665  2sqlem3  15669  2sqlem8  15675  2sqlem10  15677  structgrssvtx  15716  structgrssiedg  15717  ushgruhgr  15751  uhgrun  15757  incistruhgr  15761  upgrop  15775  upgruhgr  15782  umgrupgr  15783  umgrnloopvv  15785  umgr0e  15786  upgr1edc  15789  upgrun  15792  umgrun  15794  fnmptd  15879  bj-sels  15988  bj-nnelon  16033  2omap  16071  pw1map  16073  pwle2  16076  pwf1oexmid  16077  pw1nct  16081  nninfall  16087  nninfsellemdc  16088  nninfself  16091  nnnninfex  16100  nninfnfiinf  16101  refeq  16108  isomninnlem  16110  cvgcmp2nlemabs  16112  trilpolemlt1  16121  trirec0  16124  apdifflemf  16126  apdifflemr  16127  apdiff  16128  iswomninnlem  16129  iswomni0  16131  ismkvnnlem  16132  reap0  16138  cndcap  16139