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  706  mpbir2and  944  pm3.12dc  958  mpbir3and  1180  pm5.15dc  1389  eqeltrd  2254  eqnetrd  2371  3netr4d  2380  r19.30dc  2624  sbcne12g  3077  eqsstrd  3193  3sstr4d  3202  eqbrtrd  4027  3brtr4d  4037  snelpwi  4214  prelpwi  4216  pwel  4220  ordelon  4385  onin  4388  elelsuc  4411  onsuc  4502  onsucb  4504  onintonm  4518  omsinds  4623  sosng  4701  relssdv  4720  eqbrrdv  4725  eqrelrdv2  4727  relsnopg  4732  breldmg  4835  elrnmptdv  4883  iss  4955  xpimasn  5079  elxp4  5118  elxp5  5119  iotam  5210  funssres  5260  f0rn0  5412  sefvex  5538  fvun1  5584  eqfnfvd  5618  fvimacnvi  5632  fvimacnv  5633  fvelrn  5649  fmpt3d  5674  fmpt2d  5680  resflem  5682  fmptco  5684  fsn  5690  ftpg  5702  fconst2g  5733  funfvima3  5752  elabrexg  5761  foeqcnvco  5793  f1eqcocnv  5794  fliftfun  5799  fliftfund  5800  fliftval  5803  riota5f  5857  f1ofveu  5865  f1ocnvd  6075  f1opw2  6079  off  6097  offval2  6100  ofrfval2  6101  caofref  6106  caofinvl  6107  elxp6  6172  cnvf1olem  6227  f2ndf  6229  f1od2  6238  tposf12  6272  smores2  6297  tfrlemisucaccv  6328  tfrlemibfn  6331  tfr1onlemsucaccv  6344  tfr1onlembfn  6347  tfrcllemsucaccv  6357  tfrcllembfn  6360  tfrcl  6367  tfri3  6370  frecabcl  6402  nnsucsssuc  6495  ersym  6549  ertr  6552  swoer  6565  erth  6581  riinerm  6610  qliftfund  6620  eroprf  6630  ecopoverg  6638  th3qlem1  6639  elmapssres  6675  mapss  6693  fdiagfn  6694  ixpssmap2g  6729  mapsnf1o  6739  f1dom2g  6758  dom3d  6776  fopwdom  6838  mapxpen  6850  nndomo  6866  dif1en  6881  findcard2  6891  findcard2s  6892  diffisn  6895  fimax2gtrilemstep  6902  fientri3  6916  fiintim  6930  f1dmvrnfibi  6945  sbthlemi6  6963  elfir  6974  fifo  6981  supelti  7003  supsnti  7006  cnvinfex  7019  ordiso2  7036  updjud  7083  djudom  7094  difinfsn  7101  ctssdc  7114  enumctlemm  7115  enumct  7116  enomnilem  7138  fodjuf  7145  ismkvnex  7155  omnimkv  7156  enmkvlem  7161  enwomnilem  7169  nninfdcinf  7171  nninfwlporlem  7173  isnumi  7183  exmidfodomrlemrALT  7204  djudoml  7220  djudomr  7221  netap  7255  2omotaplemap  7258  2omotaplemst  7259  exmidapne  7261  cc2lem  7267  cc3  7269  ltsopi  7321  pitri3or  7323  ltdcpi  7324  indpi  7343  enqdc  7362  enqdc1  7363  addcmpblnq  7368  mulcanenq  7386  recrecnq  7395  nqtri3or  7397  ltdcnq  7398  ltsonq  7399  ltaddnq  7408  subhalfnqq  7415  archnqq  7418  prarloclemarch2  7420  enq0tr  7435  nqnq0  7442  addcmpblnq0  7444  mulcanenq0ec  7446  nnnq0lem1  7447  nqpnq0nq  7454  nq0m0r  7457  nq02m  7466  prarloclemlt  7494  prarloclemcalc  7503  addlocpr  7537  nqprl  7552  nqpru  7553  addnqprlemrl  7558  addnqprlemru  7559  prmuloclemcalc  7566  mullocprlem  7571  mulnqprlemrl  7574  mulnqprlemru  7575  1idprl  7591  1idpru  7592  ltaddpr  7598  ltexprlemm  7601  ltexprlemopl  7602  ltexprlemopu  7604  ltexprlemdisj  7607  ltexprlemrl  7611  ltexprlemru  7613  addcanprleml  7615  addcanprlemu  7616  addcanprg  7617  prplnqu  7621  recexprlemloc  7632  recexprlem1ssl  7634  recexprlem1ssu  7635  aptiprleml  7640  aptiprlemu  7641  archpr  7644  cauappcvgprlemm  7646  cauappcvgprlemopl  7647  cauappcvgprlemloc  7653  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  cauappcvgprlem1  7660  cauappcvgprlem2  7661  caucvgprlemnkj  7667  caucvgprlemopl  7670  caucvgprlemloc  7676  caucvgprlemladdfu  7678  caucvgprlem2  7681  caucvgprprlemnkltj  7690  caucvgprprlemopl  7698  caucvgprprlemloc  7704  caucvgprprlemexbt  7707  caucvgprprlemaddq  7709  caucvgprprlem2  7711  suplocexprlemmu  7719  suplocexprlemru  7720  suplocexprlemloc  7722  suplocexprlemlub  7725  prsrlem1  7743  0idsr  7768  1idsr  7769  recexgt0sr  7774  archsr  7783  prsradd  7787  caucvgsrlemcau  7794  caucvgsrlembound  7795  caucvgsrlemoffgt1  7800  suplocsrlemb  7807  suplocsrlempr  7808  suplocsrlem  7809  pitonnlem1p1  7847  pitonn  7849  pitoregt0  7850  peano2nnnn  7854  recidpirq  7859  axcaucvglemval  7898  leid  8043  nltled  8080  readdcan  8099  addneintrd  8147  addneintr2d  8148  pncan  8165  subsub2  8187  subsub4  8192  negned  8267  subne0d  8279  subneintrd  8314  subneintr2d  8316  subeq0bd  8338  subdi  8344  gt0add  8532  rimul  8544  rereim  8545  ltmul1a  8550  apreim  8562  apirr  8564  mulap0r  8574  msqge0  8575  mulge0  8578  gt0ap0  8585  ltap  8592  subap0d  8603  recexaplem2  8611  mulap0bad  8618  mulap0bbd  8619  mul0eqap  8629  divrecap  8647  div0ap  8661  div1  8662  recrecap  8668  divdivdivap  8672  ddcanap  8685  rerecclap  8689  div2negap  8694  diveqap1bd  8795  recgt0  8809  prodgt0  8811  lemul1a  8817  recp1lt1  8858  squeeze0  8863  peano2nn  8933  div4p1lem1div2  9174  arch  9175  peano2z  9291  peano2zm  9293  ztri3or  9298  nn0n0n1ge2  9325  zextle  9346  gtndiv  9350  suprzclex  9353  nn0ind-raph  9372  uzid  9544  uzneg  9548  uztric  9551  uz11  9552  eluzp1l  9554  qdivcl  9645  irrmul  9649  rpnegap  9688  negelrpd  9690  ledivge1le  9728  mul2lt0rlt0  9761  mul2lt0rgt0  9762  nn0ledivnn  9769  ltpnf  9782  mnflt  9785  pnfge  9791  mnfle  9794  xrlttr  9797  xrltso  9798  xrlttri3  9799  xrleid  9802  xaddass2  9872  xltadd1  9878  xlt2add  9882  xleaddadd  9889  iccf1o  10006  fztri3or  10041  fznlem  10043  fzn  10044  fzsplit2  10052  fznatpl1  10078  uzsplit  10094  fseq1p1m1  10096  fzm1  10102  fznn0sub2  10130  difelfznle  10137  1fv  10141  fzodcel  10154  fzospliti  10178  fzouzsplit  10181  eluzgtdifelfzo  10199  exfzdc  10242  subfzo0  10244  exbtwnz  10253  qbtwnrelemcalc  10258  flqlelt  10278  qfraclt1  10282  qfracge0  10283  flqltnz  10289  btwnzge0  10302  flhalf  10304  ceiqle  10315  intfracq  10322  mulqmod0  10332  modqge0  10334  modqlt  10335  modqid  10351  modqid0  10352  m1modge3gt1  10373  modqltm1p1mod  10378  q2txmodxeq0  10386  modaddmodlo  10390  modsumfzodifsn  10398  addmodlteq  10400  frecuzrdgtcl  10414  frecuzrdgtclt  10423  uzennn  10438  uzsinds  10444  seqf  10463  seqf2  10466  monoord2  10479  iseqf1olemqk  10496  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  seq3f1olemqsumkj  10500  seq3f1olemqsum  10502  seq3f1olemstep  10503  seq3f1oleml  10505  ser3le  10520  exp3vallem  10523  exp3val  10524  expp1  10529  expcllem  10533  ltexp2a  10574  leexp2a  10575  nn0ltexp2  10691  faclbnd  10723  faclbnd2  10724  faclbnd3  10725  bcval5  10745  bcpasc  10748  hashennn  10762  fihasheqf1oi  10769  hashsng  10780  fihashfn  10782  hashun  10787  fihashss  10798  fihashssdif  10800  hashfz  10803  hashxp  10808  fimaxq  10809  zfz1isolem1  10822  seq3coll  10824  shftfn  10835  cjth  10857  cjmulrcl  10898  reim0bd  10955  rerebd  10956  cjrebd  10957  caucvgre  10992  cvg1nlemcxze  10993  cvg1nlemcau  10995  cvg1nlemres  10996  recvguniq  11006  resqrexlemover  11021  resqrexlemdec  11022  resqrexlemgt0  11031  resqrexlemoverl  11032  resqrexlemglsq  11033  rersqrtthlem  11041  sqrtgt0  11045  leabs  11085  absexpzap  11091  absle  11100  recvalap  11108  abstri  11115  abs2dif  11117  amgm2  11129  absne0d  11198  maxleim  11216  maxabslemab  11217  maxabslemlub  11218  maxltsup  11229  zmaxcl  11235  fimaxre2  11237  minmax  11240  rpmincl  11248  bdtrilem  11249  bdtri  11250  xrmaxleim  11254  xrmaxiflemcom  11259  xrmaxltsup  11268  xrmaxadd  11271  xrminmax  11275  xrminrpcl  11284  climconst  11300  climuni  11303  2clim  11311  climcn1  11318  climcn2  11319  reccn2ap  11323  climge0  11335  climle  11344  climsqz  11345  climsqz2  11346  serf0  11362  summodclem3  11390  summodclem2a  11391  fsumcl2lem  11408  sumpr  11423  sumtp  11424  fsum0diaglem  11450  mptfzshft  11452  fsumle  11473  fsumlt  11474  divcnv  11507  trireciplem  11510  expcnvap0  11512  expcnv  11514  explecnv  11515  geosergap  11516  cvgratnnlembern  11533  cvgratnnlemabsle  11537  cvgratnnlemsumlt  11538  cvgratz  11542  cvgratgt0  11543  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  clim2divap  11550  prodmodclem3  11585  prodmodclem2a  11586  fprodseq  11593  fprodmul  11601  fprodfac  11625  fprodconst  11630  fprodap0  11631  fprodap0f  11646  fprodle  11650  eftcl  11664  ef0lem  11670  efsub  11691  eftlub  11700  eflegeo  11711  tanval2ap  11723  sinadd  11746  cos2t  11760  cos2tsin  11761  sin01bnd  11767  cos01bnd  11768  eirraplem  11786  dvdsval2  11799  dvdsdc  11807  dvds0lem  11810  zdvdsdc  11821  dvdscmulr  11829  dvdsmulcr  11830  dvdslelemd  11851  divconjdvds  11857  dvdsext  11863  fzm1ndvds  11864  dvdsmod  11870  oexpneg  11884  2tp1odd  11891  mulsucdiv2z  11892  2teven  11894  zeo5  11895  opeo  11904  omeo  11905  nn0ob  11915  divalglemnqt  11927  zsupcllemstep  11948  zsupcl  11950  zssinfcl  11951  infssuzex  11952  infssuzcldc  11954  suprzubdc  11955  nninfdcex  11956  gcddvds  11966  dvdslegcd  11967  gcdneg  11985  bezoutlemnewy  11999  bezoutlemstep  12000  bezoutlema  12002  bezoutlemb  12003  bezoutlemmo  12009  bezoutlemle  12011  bezoutlemsup  12012  dfgcd3  12013  bezout  12014  dfgcd2  12017  uzwodc  12040  lcmcllem  12069  lcmneg  12076  lcmgcdlem  12079  lcmdvds  12081  lcmid  12082  3lcm2e6woprm  12088  6lcm4e12  12089  ncoprmgcdne1b  12091  mulgcddvds  12096  divgcdcoprmex  12104  cncongr1  12105  cncongr2  12106  isprm2lem  12118  prmind2  12122  dvdsnprmd  12127  prm2orodd  12128  sqnprm  12138  isprm5lem  12143  rpexp  12155  sqrt2irrlem  12163  oddpwdclemdc  12175  sqrt2irraplemnn  12181  qnumdencoprm  12195  qeqnumdivden  12196  nn0gcdsq  12202  nn0sqrtelqelz  12208  nonsq  12209  phicl2  12216  phibnd  12219  hashdvds  12223  phiprmpw  12224  phimullem  12227  eulerthlemrprm  12231  eulerthlema  12232  eulerthlemth  12234  prmdiveq  12238  hashgcdlem  12240  odzdvds  12247  modprminv  12251  nnnn0modprm0  12257  modprmn0modprm0  12258  pythagtriplem10  12271  pythagtriplem19  12284  pythagtrip  12285  pcpre1  12294  pcpremul  12295  pceu  12297  pcmul  12303  pcdiv  12304  pcqmul  12305  pcqdiv  12309  pcexp  12311  pcdvdsb  12321  pcidlem  12324  pcdvdstr  12328  pcgcd1  12329  pc2dvds  12331  pcprmpw2  12334  difsqpwdvds  12339  pcaddlem  12340  pcadd  12341  pcmpt  12343  pcmptdvds  12345  pcprod  12346  fldivp1  12348  pcfaclem  12349  pcfac  12350  pcbc  12351  qexpz  12352  pockthlem  12356  pockthg  12357  1arithlem4  12366  1arith  12367  1arith2  12368  4sqlem6  12383  4sqlem8  12385  4sqlem9  12386  4sqlem10  12387  znnen  12401  ennnfonelemk  12403  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ennnfonelemrnh  12419  ennnfonelemfun  12420  ennnfonelemf1  12421  ennnfonelemrn  12422  ennnfonelemnn0  12425  ctinfomlemom  12430  ctiunctlemudc  12440  unct  12445  omctfn  12446  ssnnctlemct  12449  nninfdclemp1  12453  nninfdc  12456  structfung  12481  setsfun  12499  setsfun0  12500  setscom  12504  setsslid  12515  imasaddfnlemg  12740  imasaddvallemg  12741  mgmsscl  12785  plusffng  12789  mgmplusf  12790  mgm0  12793  mgm1  12794  opifismgmdc  12795  sgrp1  12821  mndpfo  12844  mndfo  12845  mnd1  12852  0subm  12876  mhmima  12880  grpinvfng  12922  isgrpinv  12931  grpinvid  12935  grpinvf1o  12945  grpinvadd  12953  grpsubf  12954  grpsubsub4  12968  grplactcnv  12977  grp1  12981  grp1inv  12982  mulgfng  12992  subginv  13046  resgrpisgrp  13060  subgintm  13063  0subg  13064  0nsg  13079  srgideu  13160  srgidmlem  13166  srgpcomp  13178  srg1expzeq1  13183  ringcl  13201  ringideu  13205  ringidmlem  13210  ringnegl  13233  ringnegr  13234  ring1  13241  opprringbg  13255  dvdsrd  13268  dvdsr01  13278  isunitd  13280  unitinvcl  13297  unitinvinv  13298  unitnegcl  13304  nzrunit  13334  lringuplu  13342  subrgsubm  13360  subrgintm  13369  aprsym  13379  scaffng  13404  lmodscaf  13405  lsssn0  13461  lss1d  13475  lssintclm  13476  cnfldneg  13506  zringinvg  13533  baspartn  13589  eltg3i  13595  tgclb  13604  topbas  13606  2basgeng  13621  topcld  13648  0cld  13651  uncld  13652  neif  13680  elnei  13691  0nei  13705  restbasg  13707  iscnp4  13757  cnpnei  13758  cnclima  13762  cncnp  13769  cnrest2r  13776  cndis  13780  lmff  13788  lmtopcnp  13789  txbas  13797  txopn  13804  txcnp  13810  upxp  13811  txdis1cn  13817  cnmpt11  13822  cnmpt21  13830  psmetge0  13870  xmetge0  13904  xmettpos  13909  xmetrtri  13915  metrtri  13916  xblpnfps  13937  xblpnf  13938  blfps  13948  blf  13949  ssblps  13964  ssbl  13965  blbas  13972  metss2  14037  xmettxlem  14048  xmettx  14049  qtopbas  14061  divcnap  14094  cncfss  14109  cdivcncfap  14126  expcncf  14131  cnopnap  14133  dedekindeulemuub  14134  dedekindeulemlu  14138  dedekindeu  14140  suplociccex  14142  dedekindicclemuub  14143  dedekindicclemlu  14147  dedekindicclemicc  14149  ivthinclemlopn  14153  ivthinclemuopn  14155  ivthinc  14160  ellimc3apf  14168  limcimolemlt  14172  limcimo  14173  limcresi  14174  cnplimclemle  14176  reldvg  14187  dvfgg  14196  dvidlemap  14199  dvcjbr  14211  dvcj  14212  dvrecap  14216  dveflem  14226  dvef  14227  reeff1oleme  14232  pilem3  14243  sinq34lt0t  14291  cosq14gt0  14292  coseq0q4123  14294  tangtx  14298  sincosq1eq  14299  cosordlem  14309  logdivlti  14341  relogbval  14408  relogbzcl  14409  nnlogbexp  14416  logbgcd1irr  14424  logbgcd1irraplemexp  14425  logbgcd1irraplemap  14426  zabsle1  14439  lgslem1  14440  lgsval  14444  lgsfvalg  14445  lgsfcl2  14446  lgsval2lem  14450  lgscl1  14463  lgsmod  14466  lgsdir2lem5  14472  lgsdir2  14473  lgsdilem2  14476  lgsdi  14477  lgsne0  14478  lgseisenlem1  14489  lgseisenlem2  14490  2lgsoddprmlem2  14493  2sqlem3  14503  2sqlem8  14509  2sqlem10  14511  fnmptd  14595  bj-sels  14705  bj-nnelon  14750  pwle2  14787  pwf1oexmid  14788  pw1nct  14791  nninfall  14797  nninfsellemdc  14798  nninfself  14801  refeq  14815  isomninnlem  14817  cvgcmp2nlemabs  14819  trilpolemlt1  14828  trirec0  14831  apdifflemf  14833  apdifflemr  14834  apdiff  14835  iswomninnlem  14836  iswomni0  14838  ismkvnnlem  14839  reap0  14845