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  707  pm4.55dc  940  mpbir2and  946  pm3.12dc  960  mpbir3and  1182  pm5.15dc  1408  eqeltrd  2281  eqnetrd  2399  3netr4d  2408  r19.30dc  2652  raleqtrrdv  2711  rexeqtrrdv  2712  sbcne12g  3110  eqsstrd  3228  3sstr4d  3237  eqbrtrd  4065  3brtr4d  4075  snelpwi  4255  prelpwi  4257  pwel  4261  ordelon  4428  onin  4431  elelsuc  4454  onsuc  4547  onsucb  4549  onintonm  4563  omsinds  4668  sosng  4746  relssdv  4765  eqbrrdv  4770  eqrelrdv2  4772  relsnopg  4777  breldmg  4882  elrnmptdv  4930  iss  5002  xpimasn  5128  elxp4  5167  elxp5  5168  iotam  5260  funssres  5310  f0rn0  5464  fimadmfo  5501  sefvex  5591  fvun1  5639  eqfnfvd  5674  fvimacnvi  5688  fvimacnv  5689  fvelrn  5705  fmpt3d  5730  fmpt2d  5736  resflem  5738  fmptco  5740  fsn  5746  ftpg  5758  fconst2g  5789  funfvima3  5808  elabrexg  5817  foeqcnvco  5849  f1eqcocnv  5850  fliftfun  5855  fliftfund  5856  fliftval  5859  riota5f  5914  f1ofveu  5922  f1ocnvd  6138  f1opw2  6142  off  6161  offval2  6164  ofrfval2  6165  offveq  6169  caofref  6173  caofinvl  6174  elxp6  6245  cnvf1olem  6300  f2ndf  6302  f1od2  6311  tposf12  6345  smores2  6370  tfrlemisucaccv  6401  tfrlemibfn  6404  tfr1onlemsucaccv  6417  tfr1onlembfn  6420  tfrcllemsucaccv  6430  tfrcllembfn  6433  tfrcl  6440  tfri3  6443  frecabcl  6475  nnsucsssuc  6568  ersym  6622  ertr  6625  swoer  6638  erth  6656  riinerm  6685  qliftfund  6695  eroprf  6705  ecopoverg  6713  th3qlem1  6714  elmapssres  6750  mapss  6768  fdiagfn  6769  ixpssmap2g  6804  mapsnf1o  6814  f1dom2g  6833  dom3d  6851  pw2f1odclem  6913  fopwdom  6915  mapxpen  6927  nndomo  6943  dif1en  6958  findcard2  6968  findcard2s  6969  diffisn  6972  fimax2gtrilemstep  6979  fientri3  6994  tpfidceq  7009  fiintim  7010  opabfi  7017  f1dmvrnfibi  7028  sbthlemi6  7046  elfir  7057  fifo  7064  supelti  7086  supsnti  7089  cnvinfex  7102  ordiso2  7119  updjud  7166  djudom  7177  difinfsn  7184  ctssdc  7197  enumctlemm  7198  enumct  7199  nninfninc  7207  enomnilem  7222  fodjuf  7229  ismkvnex  7239  omnimkv  7240  enmkvlem  7245  enwomnilem  7253  nninfdcinf  7255  nninfwlporlem  7257  isnumi  7271  exmidfodomrlemrALT  7293  finacn  7298  djudoml  7313  djudomr  7314  netap  7348  2omotaplemap  7351  2omotaplemst  7352  exmidapne  7354  cc2lem  7360  cc3  7362  ltsopi  7415  pitri3or  7417  ltdcpi  7418  indpi  7437  enqdc  7456  enqdc1  7457  addcmpblnq  7462  mulcanenq  7480  recrecnq  7489  nqtri3or  7491  ltdcnq  7492  ltsonq  7493  ltaddnq  7502  subhalfnqq  7509  archnqq  7512  prarloclemarch2  7514  enq0tr  7529  nqnq0  7536  addcmpblnq0  7538  mulcanenq0ec  7540  nnnq0lem1  7541  nqpnq0nq  7548  nq0m0r  7551  nq02m  7560  prarloclemlt  7588  prarloclemcalc  7597  addlocpr  7631  nqprl  7646  nqpru  7647  addnqprlemrl  7652  addnqprlemru  7653  prmuloclemcalc  7660  mullocprlem  7665  mulnqprlemrl  7668  mulnqprlemru  7669  1idprl  7685  1idpru  7686  ltaddpr  7692  ltexprlemm  7695  ltexprlemopl  7696  ltexprlemopu  7698  ltexprlemdisj  7701  ltexprlemrl  7705  ltexprlemru  7707  addcanprleml  7709  addcanprlemu  7710  addcanprg  7711  prplnqu  7715  recexprlemloc  7726  recexprlem1ssl  7728  recexprlem1ssu  7729  aptiprleml  7734  aptiprlemu  7735  archpr  7738  cauappcvgprlemm  7740  cauappcvgprlemopl  7741  cauappcvgprlemloc  7747  cauappcvgprlemladdfu  7749  cauappcvgprlemladdfl  7750  cauappcvgprlem1  7754  cauappcvgprlem2  7755  caucvgprlemnkj  7761  caucvgprlemopl  7764  caucvgprlemloc  7770  caucvgprlemladdfu  7772  caucvgprlem2  7775  caucvgprprlemnkltj  7784  caucvgprprlemopl  7792  caucvgprprlemloc  7798  caucvgprprlemexbt  7801  caucvgprprlemaddq  7803  caucvgprprlem2  7805  suplocexprlemmu  7813  suplocexprlemru  7814  suplocexprlemloc  7816  suplocexprlemlub  7819  prsrlem1  7837  0idsr  7862  1idsr  7863  recexgt0sr  7868  archsr  7877  prsradd  7881  caucvgsrlemcau  7888  caucvgsrlembound  7889  caucvgsrlemoffgt1  7894  suplocsrlemb  7901  suplocsrlempr  7902  suplocsrlem  7903  pitonnlem1p1  7941  pitonn  7943  pitoregt0  7944  peano2nnnn  7948  recidpirq  7953  axcaucvglemval  7992  leid  8138  nltled  8175  readdcan  8194  addneintrd  8242  addneintr2d  8243  pncan  8260  subsub2  8282  subsub4  8287  negned  8362  subne0d  8374  subneintrd  8409  subneintr2d  8411  subeq0bd  8433  subdi  8439  gt0add  8628  rimul  8640  rereim  8641  ltmul1a  8646  apreim  8658  apirr  8660  mulap0r  8670  msqge0  8671  mulge0  8674  gt0ap0  8681  ltap  8688  subap0d  8699  recexaplem2  8707  mulap0bad  8714  mulap0bbd  8715  mul0eqap  8725  divrecap  8743  div0ap  8757  div1  8758  recrecap  8764  divdivdivap  8768  ddcanap  8781  rerecclap  8785  div2negap  8790  diveqap1bd  8891  recgt0  8905  prodgt0  8907  lemul1a  8913  recp1lt1  8954  squeeze0  8959  peano2nn  9030  div4p1lem1div2  9273  arch  9274  peano2z  9390  peano2zm  9392  ztri3or  9397  nn0n0n1ge2  9425  zextle  9446  gtndiv  9450  suprzclex  9453  nn0ind-raph  9472  uzid  9644  uzneg  9649  uztric  9652  uz11  9653  eluzp1l  9655  qdivcl  9746  irrmul  9750  irrmulap  9751  rpnegap  9790  negelrpd  9792  ledivge1le  9830  mul2lt0rlt0  9863  mul2lt0rgt0  9864  nn0ledivnn  9871  ltpnf  9884  mnflt  9887  pnfge  9893  mnfle  9896  xrlttr  9899  xrltso  9900  xrlttri3  9901  xrleid  9904  xaddass2  9974  xltadd1  9980  xlt2add  9984  xleaddadd  9991  iccf1o  10108  fztri3or  10143  fznlem  10145  fzn  10146  fzsplit2  10154  fznatpl1  10180  uzsplit  10196  fseq1p1m1  10198  fzm1  10204  fznn0sub2  10232  difelfznle  10239  1fv  10243  fzodcel  10257  fzospliti  10281  fzouzsplit  10284  eluzgtdifelfzo  10307  exfzdc  10350  subfzo0  10352  zsupcllemstep  10353  zsupcl  10355  zssinfcl  10356  infssuzex  10357  infssuzcldc  10359  suprzubdc  10360  nninfdcex  10361  qdcle  10370  exbtwnz  10374  qbtwnrelemcalc  10379  flqlelt  10400  qfraclt1  10404  qfracge0  10405  flqltnz  10411  btwnzge0  10424  flhalf  10426  fldiv4lem1div2uz2  10430  ceiqle  10439  intfracq  10446  mulqmod0  10456  modqge0  10458  modqlt  10459  modqid  10475  modqid0  10476  m1modge3gt1  10497  modqltm1p1mod  10502  q2txmodxeq0  10510  modaddmodlo  10514  modsumfzodifsn  10522  addmodlteq  10524  frecuzrdgtcl  10538  frecuzrdgtclt  10547  uzennn  10562  uzsinds  10570  seqf  10590  seqf2  10594  monoord2  10612  iseqf1olemqk  10633  iseqf1olemjpcl  10634  iseqf1olemqpcl  10635  seq3f1olemqsumkj  10637  seq3f1olemqsum  10639  seq3f1olemstep  10640  seq3f1oleml  10642  seqf1oglem1  10645  ser3le  10663  exp3vallem  10666  exp3val  10667  expp1  10672  expcllem  10676  ltexp2a  10717  leexp2a  10718  nn0ltexp2  10835  faclbnd  10867  faclbnd2  10868  faclbnd3  10869  bcval5  10889  bcpasc  10892  hashennn  10906  fihasheqf1oi  10913  hashsng  10924  fihashfn  10926  hashun  10931  fihashss  10942  fihashssdif  10944  hashfz  10947  hashxp  10952  fimaxq  10953  zfz1isolem1  10966  seq3coll  10968  wrdf  10975  wrdlenge2n0  11004  fstwrdne0  11008  wrdred1hash  11012  ccatvalfn  11032  ccatsymb  11033  ccatlid  11037  ccatrid  11038  ccatrn  11040  shftfn  11054  cjth  11076  cjmulrcl  11117  reim0bd  11174  rerebd  11175  cjrebd  11176  caucvgre  11211  cvg1nlemcxze  11212  cvg1nlemcau  11214  cvg1nlemres  11215  recvguniq  11225  resqrexlemover  11240  resqrexlemdec  11241  resqrexlemgt0  11250  resqrexlemoverl  11251  resqrexlemglsq  11252  rersqrtthlem  11260  sqrtgt0  11264  leabs  11304  absexpzap  11310  absle  11319  recvalap  11327  abstri  11334  abs2dif  11336  amgm2  11348  absne0d  11417  maxleim  11435  maxabslemab  11436  maxabslemlub  11437  maxltsup  11448  zmaxcl  11454  fimaxre2  11457  minmax  11460  rpmincl  11468  bdtrilem  11469  bdtri  11470  xrmaxleim  11474  xrmaxiflemcom  11479  xrmaxltsup  11488  xrmaxadd  11491  xrminmax  11495  xrminrpcl  11504  climconst  11520  climuni  11523  2clim  11531  climcn1  11538  climcn2  11539  reccn2ap  11543  climge0  11555  climle  11564  climsqz  11565  climsqz2  11566  serf0  11582  summodclem3  11610  summodclem2a  11611  fsumcl2lem  11628  sumpr  11643  sumtp  11644  fsum0diaglem  11670  mptfzshft  11672  fsumle  11693  fsumlt  11694  divcnv  11727  trireciplem  11730  expcnvap0  11732  expcnv  11734  explecnv  11735  geosergap  11736  cvgratnnlembern  11753  cvgratnnlemabsle  11757  cvgratnnlemsumlt  11758  cvgratz  11762  cvgratgt0  11763  mertenslemi1  11765  mertenslem2  11766  mertensabs  11767  clim2divap  11770  prodmodclem3  11805  prodmodclem2a  11806  fprodseq  11813  fprodmul  11821  fprodfac  11845  fprodconst  11850  fprodap0  11851  fprodap0f  11866  fprodle  11870  eftcl  11884  ef0lem  11890  efsub  11911  eftlub  11920  eflegeo  11931  tanval2ap  11943  sinadd  11966  cos2t  11980  cos2tsin  11981  sin01bnd  11987  cos01bnd  11988  eirraplem  12007  dvdsval2  12020  dvdsdc  12028  dvds0lem  12031  zdvdsdc  12042  dvdscmulr  12050  dvdsmulcr  12051  fsumdvds  12072  dvdslelemd  12073  divconjdvds  12079  dvdsext  12085  fzm1ndvds  12086  dvdsmod  12092  3dvds  12094  oexpneg  12107  2tp1odd  12114  mulsucdiv2z  12115  2teven  12117  zeo5  12118  opeo  12127  omeo  12128  nn0ob  12138  divalglemnqt  12150  bitsdc  12177  bits0o  12180  bitsfzolem  12184  bitsfzo  12185  bitsmod  12186  bitscmp  12188  bitsinv1lem  12191  gcddvds  12203  dvdslegcd  12204  gcdneg  12222  bezoutlemnewy  12236  bezoutlemstep  12237  bezoutlema  12239  bezoutlemb  12240  bezoutlemmo  12246  bezoutlemle  12248  bezoutlemsup  12249  dfgcd3  12250  bezout  12251  dfgcd2  12254  uzwodc  12277  lcmcllem  12308  lcmneg  12315  lcmgcdlem  12318  lcmdvds  12320  lcmid  12321  3lcm2e6woprm  12327  6lcm4e12  12328  ncoprmgcdne1b  12330  mulgcddvds  12335  divgcdcoprmex  12343  cncongr1  12344  cncongr2  12345  isprm2lem  12357  prmind2  12361  dvdsnprmd  12366  prm2orodd  12367  sqnprm  12377  isprm5lem  12382  rpexp  12394  sqrt2irrlem  12402  oddpwdclemdc  12414  sqrt2irraplemnn  12420  qnumdencoprm  12434  qeqnumdivden  12435  nn0gcdsq  12441  nn0sqrtelqelz  12447  nonsq  12448  phicl2  12455  phibnd  12458  hashdvds  12462  phiprmpw  12463  phimullem  12466  eulerthlemrprm  12470  eulerthlema  12471  eulerthlemth  12473  prmdiveq  12477  hashgcdlem  12479  odzdvds  12487  modprminv  12491  nnnn0modprm0  12497  modprmn0modprm0  12498  pythagtriplem10  12511  pythagtriplem19  12524  pythagtrip  12525  pcpre1  12534  pcpremul  12535  pceu  12537  pcmul  12543  pcdiv  12544  pcqmul  12545  pcqdiv  12549  pcexp  12551  pcdvdsb  12562  pcidlem  12565  pcdvdstr  12569  pcgcd1  12570  pc2dvds  12572  pcprmpw2  12575  difsqpwdvds  12580  pcaddlem  12581  pcadd  12582  pcadd2  12583  pcmpt  12585  pcmptdvds  12587  pcprod  12588  fldivp1  12590  pcfaclem  12591  pcfac  12592  pcbc  12593  qexpz  12594  pockthlem  12598  pockthg  12599  1arithlem4  12608  1arith  12609  1arith2  12610  4sqlem6  12625  4sqlem8  12627  4sqlem9  12628  4sqlem10  12629  4sqexercise1  12640  4sqexercise2  12641  4sqlemsdc  12642  4sqlem11  12643  4sqlem12  12644  4sqlem15  12647  4sqlem16  12648  4sqlem17  12649  znnen  12688  ennnfonelemk  12690  ennnfonelemkh  12702  ennnfonelemhf1o  12703  ennnfonelemrnh  12706  ennnfonelemfun  12707  ennnfonelemf1  12708  ennnfonelemrn  12709  ennnfonelemnn0  12712  ctinfomlemom  12717  ctiunctlemudc  12727  unct  12732  omctfn  12733  ssnnctlemct  12736  nninfdclemp1  12740  nninfdc  12743  structfung  12768  setsfun  12786  setsfun0  12787  setscom  12791  strslfv3  12797  setsslid  12802  pwsdiagel  13047  pwssnf1o  13048  imasaddfnlemg  13064  imasaddvallemg  13065  mgmsscl  13111  plusffng  13115  mgmplusf  13116  mgm0  13119  mgm1  13120  opifismgmdc  13121  gsumfzval  13141  gsumprval  13149  sgrp1  13161  issgrpd  13162  prdsplusgsgrpcl  13164  mndpfo  13188  mndfo  13189  prdsplusgcl  13196  prdsidlem  13197  mnd1  13205  0subm  13234  mhmima  13241  grpinvfng  13294  isgrpinv  13304  grpinvid  13310  grpinvf1o  13320  grpinvadd  13328  grpsubf  13329  grpsubsub4  13343  grplactcnv  13352  grp1  13356  grp1inv  13357  prdsinvlem  13358  prdsinvgd  13360  qusgrp2  13367  mulgfng  13378  subginv  13435  resgrpisgrp  13449  subgintm  13452  0subg  13453  0nsg  13468  qusinv  13490  ghminv  13504  ghmrn  13511  ghmeql  13521  ghmnsgima  13522  kerf1ghm  13528  conjnmz  13533  rngass  13619  rngmneg1  13627  rngmneg2  13628  qusrng  13638  srgideu  13652  srgidmlem  13658  srgpcomp  13670  srg1expzeq1  13675  ringcl  13693  ringideu  13697  ringidmlem  13702  ringnegl  13731  ringnegr  13732  ring1  13739  qusring2  13746  opprringbg  13760  dvdsrd  13774  dvdsr01  13784  isunitd  13786  unitinvcl  13803  unitinvinv  13804  unitnegcl  13810  rhmmul  13844  rhmf1o  13848  nzrunit  13868  lringuplu  13876  subrngintm  13892  subrgsubm  13914  subrgintm  13923  aprsym  13964  scaffng  13989  lmodscaf  13990  lsssn0  14050  lss1d  14063  lssintclm  14064  lspval  14070  lspcl  14071  lspsnid  14087  lspprid1  14091  lspsn  14096  sraval  14117  rspcl  14171  rspssid  14172  rspssp  14174  rnglidlmmgm  14176  rnglidlmsgrp  14177  cnfldneg  14253  zringinvg  14284  expghmap  14287  znzrhfo  14328  znf1o  14331  znhash  14336  znidomb  14338  znrrg  14340  psrbagfi  14353  psraddcl  14360  psr0cl  14361  psrnegcl  14363  psrneg  14367  psr1clfi  14368  mplsubgfilemm  14378  mplsubgfilemcl  14379  baspartn  14440  eltg3i  14446  tgclb  14455  topbas  14457  2basgeng  14472  topcld  14499  0cld  14502  uncld  14503  neif  14531  elnei  14542  0nei  14556  restbasg  14558  iscnp4  14608  cnpnei  14609  cnclima  14613  cncnp  14620  cnrest2r  14627  cndis  14631  lmff  14639  lmtopcnp  14640  txbas  14648  txopn  14655  txcnp  14661  upxp  14662  txdis1cn  14668  cnmpt11  14673  cnmpt21  14681  psmetge0  14721  xmetge0  14755  xmettpos  14760  xmetrtri  14766  metrtri  14767  xblpnfps  14788  xblpnf  14789  blfps  14799  blf  14800  ssblps  14815  ssbl  14816  blbas  14823  metss2  14888  xmettxlem  14899  xmettx  14900  qtopbas  14912  divcnap  14955  cncfss  14973  cdivcncfap  14994  expcncf  14999  cnopnap  15001  maxcncf  15005  mincncf  15006  dedekindeulemuub  15007  dedekindeulemlu  15011  dedekindeu  15013  suplociccex  15015  dedekindicclemuub  15016  dedekindicclemlu  15020  dedekindicclemicc  15022  ivthinclemlopn  15026  ivthinclemuopn  15028  ivthinc  15033  ivthreinc  15035  hoverlt1  15039  ellimc3apf  15050  limcimolemlt  15054  limcimo  15055  limcresi  15056  cnplimclemle  15058  reldvg  15069  dvfgg  15078  dvidlemap  15081  dvidrelem  15082  dvidsslem  15083  dvcjbr  15098  dvcj  15099  dvrecap  15103  dveflem  15116  dvef  15117  elply2  15125  elplyr  15130  plycj  15151  plyreres  15154  reeff1oleme  15162  pilem3  15173  sinq34lt0t  15221  cosq14gt0  15222  coseq0q4123  15224  tangtx  15228  sincosq1eq  15229  cosordlem  15239  logdivlti  15271  relogbval  15341  relogbzcl  15342  nnlogbexp  15349  logbgcd1irr  15357  logbgcd1irraplemexp  15358  logbgcd1irraplemap  15359  wilthlem1  15370  mpodvdsmulf1o  15380  mersenne  15387  perfectlem2  15390  perfect  15391  zabsle1  15394  lgslem1  15395  lgsval  15399  lgsfvalg  15400  lgsfcl2  15401  lgsval2lem  15405  lgscl1  15418  lgsmod  15421  lgsdir2lem5  15427  lgsdir2  15428  lgsdilem2  15431  lgsdi  15432  lgsne0  15433  gausslemma2dlem0c  15446  gausslemma2dlem0h  15451  gausslemma2dlem1a  15453  gausslemma2dlem1f1o  15455  gausslemma2dlem3  15458  lgseisenlem1  15465  lgseisenlem2  15466  lgseisenlem3  15467  lgseisenlem4  15468  lgseisen  15469  lgsquadlem1  15472  lgsquadlem2  15473  lgsquadlem3  15474  lgsquad3  15479  2lgslem3b1  15493  2lgslem3c1  15494  2lgs  15499  2lgsoddprmlem2  15501  2lgsoddprm  15508  2sqlem3  15512  2sqlem8  15518  2sqlem10  15520  fnmptd  15604  bj-sels  15714  bj-nnelon  15759  2omap  15796  pwle2  15799  pwf1oexmid  15800  pw1nct  15804  nninfall  15810  nninfsellemdc  15811  nninfself  15814  nnnninfex  15823  nninfnfiinf  15824  refeq  15831  isomninnlem  15833  cvgcmp2nlemabs  15835  trilpolemlt1  15844  trirec0  15847  apdifflemf  15849  apdifflemr  15850  apdiff  15851  iswomninnlem  15852  iswomni0  15854  ismkvnnlem  15855  reap0  15861  cndcap  15862