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  1400  eqeltrd  2273  eqnetrd  2391  3netr4d  2400  r19.30dc  2644  raleqtrrdv  2703  rexeqtrrdv  2704  sbcne12g  3102  eqsstrd  3220  3sstr4d  3229  eqbrtrd  4056  3brtr4d  4066  snelpwi  4246  prelpwi  4248  pwel  4252  ordelon  4419  onin  4422  elelsuc  4445  onsuc  4538  onsucb  4540  onintonm  4554  omsinds  4659  sosng  4737  relssdv  4756  eqbrrdv  4761  eqrelrdv2  4763  relsnopg  4768  breldmg  4873  elrnmptdv  4921  iss  4993  xpimasn  5119  elxp4  5158  elxp5  5159  iotam  5251  funssres  5301  f0rn0  5455  fimadmfo  5492  sefvex  5582  fvun1  5630  eqfnfvd  5665  fvimacnvi  5679  fvimacnv  5680  fvelrn  5696  fmpt3d  5721  fmpt2d  5727  resflem  5729  fmptco  5731  fsn  5737  ftpg  5749  fconst2g  5780  funfvima3  5799  elabrexg  5808  foeqcnvco  5840  f1eqcocnv  5841  fliftfun  5846  fliftfund  5847  fliftval  5850  riota5f  5905  f1ofveu  5913  f1ocnvd  6129  f1opw2  6133  off  6152  offval2  6155  ofrfval2  6156  offveq  6160  caofref  6164  caofinvl  6165  elxp6  6236  cnvf1olem  6291  f2ndf  6293  f1od2  6302  tposf12  6336  smores2  6361  tfrlemisucaccv  6392  tfrlemibfn  6395  tfr1onlemsucaccv  6408  tfr1onlembfn  6411  tfrcllemsucaccv  6421  tfrcllembfn  6424  tfrcl  6431  tfri3  6434  frecabcl  6466  nnsucsssuc  6559  ersym  6613  ertr  6616  swoer  6629  erth  6647  riinerm  6676  qliftfund  6686  eroprf  6696  ecopoverg  6704  th3qlem1  6705  elmapssres  6741  mapss  6759  fdiagfn  6760  ixpssmap2g  6795  mapsnf1o  6805  f1dom2g  6824  dom3d  6842  pw2f1odclem  6904  fopwdom  6906  mapxpen  6918  nndomo  6934  dif1en  6949  findcard2  6959  findcard2s  6960  diffisn  6963  fimax2gtrilemstep  6970  fientri3  6985  tpfidceq  7000  fiintim  7001  opabfi  7008  f1dmvrnfibi  7019  sbthlemi6  7037  elfir  7048  fifo  7055  supelti  7077  supsnti  7080  cnvinfex  7093  ordiso2  7110  updjud  7157  djudom  7168  difinfsn  7175  ctssdc  7188  enumctlemm  7189  enumct  7190  nninfninc  7198  enomnilem  7213  fodjuf  7220  ismkvnex  7230  omnimkv  7231  enmkvlem  7236  enwomnilem  7244  nninfdcinf  7246  nninfwlporlem  7248  isnumi  7260  exmidfodomrlemrALT  7282  finacn  7287  djudoml  7302  djudomr  7303  netap  7337  2omotaplemap  7340  2omotaplemst  7341  exmidapne  7343  cc2lem  7349  cc3  7351  ltsopi  7404  pitri3or  7406  ltdcpi  7407  indpi  7426  enqdc  7445  enqdc1  7446  addcmpblnq  7451  mulcanenq  7469  recrecnq  7478  nqtri3or  7480  ltdcnq  7481  ltsonq  7482  ltaddnq  7491  subhalfnqq  7498  archnqq  7501  prarloclemarch2  7503  enq0tr  7518  nqnq0  7525  addcmpblnq0  7527  mulcanenq0ec  7529  nnnq0lem1  7530  nqpnq0nq  7537  nq0m0r  7540  nq02m  7549  prarloclemlt  7577  prarloclemcalc  7586  addlocpr  7620  nqprl  7635  nqpru  7636  addnqprlemrl  7641  addnqprlemru  7642  prmuloclemcalc  7649  mullocprlem  7654  mulnqprlemrl  7657  mulnqprlemru  7658  1idprl  7674  1idpru  7675  ltaddpr  7681  ltexprlemm  7684  ltexprlemopl  7685  ltexprlemopu  7687  ltexprlemdisj  7690  ltexprlemrl  7694  ltexprlemru  7696  addcanprleml  7698  addcanprlemu  7699  addcanprg  7700  prplnqu  7704  recexprlemloc  7715  recexprlem1ssl  7717  recexprlem1ssu  7718  aptiprleml  7723  aptiprlemu  7724  archpr  7727  cauappcvgprlemm  7729  cauappcvgprlemopl  7730  cauappcvgprlemloc  7736  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  cauappcvgprlem1  7743  cauappcvgprlem2  7744  caucvgprlemnkj  7750  caucvgprlemopl  7753  caucvgprlemloc  7759  caucvgprlemladdfu  7761  caucvgprlem2  7764  caucvgprprlemnkltj  7773  caucvgprprlemopl  7781  caucvgprprlemloc  7787  caucvgprprlemexbt  7790  caucvgprprlemaddq  7792  caucvgprprlem2  7794  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemloc  7805  suplocexprlemlub  7808  prsrlem1  7826  0idsr  7851  1idsr  7852  recexgt0sr  7857  archsr  7866  prsradd  7870  caucvgsrlemcau  7877  caucvgsrlembound  7878  caucvgsrlemoffgt1  7883  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  pitonnlem1p1  7930  pitonn  7932  pitoregt0  7933  peano2nnnn  7937  recidpirq  7942  axcaucvglemval  7981  leid  8127  nltled  8164  readdcan  8183  addneintrd  8231  addneintr2d  8232  pncan  8249  subsub2  8271  subsub4  8276  negned  8351  subne0d  8363  subneintrd  8398  subneintr2d  8400  subeq0bd  8422  subdi  8428  gt0add  8617  rimul  8629  rereim  8630  ltmul1a  8635  apreim  8647  apirr  8649  mulap0r  8659  msqge0  8660  mulge0  8663  gt0ap0  8670  ltap  8677  subap0d  8688  recexaplem2  8696  mulap0bad  8703  mulap0bbd  8704  mul0eqap  8714  divrecap  8732  div0ap  8746  div1  8747  recrecap  8753  divdivdivap  8757  ddcanap  8770  rerecclap  8774  div2negap  8779  diveqap1bd  8880  recgt0  8894  prodgt0  8896  lemul1a  8902  recp1lt1  8943  squeeze0  8948  peano2nn  9019  div4p1lem1div2  9262  arch  9263  peano2z  9379  peano2zm  9381  ztri3or  9386  nn0n0n1ge2  9413  zextle  9434  gtndiv  9438  suprzclex  9441  nn0ind-raph  9460  uzid  9632  uzneg  9637  uztric  9640  uz11  9641  eluzp1l  9643  qdivcl  9734  irrmul  9738  irrmulap  9739  rpnegap  9778  negelrpd  9780  ledivge1le  9818  mul2lt0rlt0  9851  mul2lt0rgt0  9852  nn0ledivnn  9859  ltpnf  9872  mnflt  9875  pnfge  9881  mnfle  9884  xrlttr  9887  xrltso  9888  xrlttri3  9889  xrleid  9892  xaddass2  9962  xltadd1  9968  xlt2add  9972  xleaddadd  9979  iccf1o  10096  fztri3or  10131  fznlem  10133  fzn  10134  fzsplit2  10142  fznatpl1  10168  uzsplit  10184  fseq1p1m1  10186  fzm1  10192  fznn0sub2  10220  difelfznle  10227  1fv  10231  fzodcel  10245  fzospliti  10269  fzouzsplit  10272  eluzgtdifelfzo  10290  exfzdc  10333  subfzo0  10335  zsupcllemstep  10336  zsupcl  10338  zssinfcl  10339  infssuzex  10340  infssuzcldc  10342  suprzubdc  10343  nninfdcex  10344  qdcle  10353  exbtwnz  10357  qbtwnrelemcalc  10362  flqlelt  10383  qfraclt1  10387  qfracge0  10388  flqltnz  10394  btwnzge0  10407  flhalf  10409  fldiv4lem1div2uz2  10413  ceiqle  10422  intfracq  10429  mulqmod0  10439  modqge0  10441  modqlt  10442  modqid  10458  modqid0  10459  m1modge3gt1  10480  modqltm1p1mod  10485  q2txmodxeq0  10493  modaddmodlo  10497  modsumfzodifsn  10505  addmodlteq  10507  frecuzrdgtcl  10521  frecuzrdgtclt  10530  uzennn  10545  uzsinds  10553  seqf  10573  seqf2  10577  monoord2  10595  iseqf1olemqk  10616  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  seq3f1olemqsumkj  10620  seq3f1olemqsum  10622  seq3f1olemstep  10623  seq3f1oleml  10625  seqf1oglem1  10628  ser3le  10646  exp3vallem  10649  exp3val  10650  expp1  10655  expcllem  10659  ltexp2a  10700  leexp2a  10701  nn0ltexp2  10818  faclbnd  10850  faclbnd2  10851  faclbnd3  10852  bcval5  10872  bcpasc  10875  hashennn  10889  fihasheqf1oi  10896  hashsng  10907  fihashfn  10909  hashun  10914  fihashss  10925  fihashssdif  10927  hashfz  10930  hashxp  10935  fimaxq  10936  zfz1isolem1  10949  seq3coll  10951  wrdf  10958  wrdlenge2n0  10987  fstwrdne0  10991  wrdred1hash  10995  shftfn  11006  cjth  11028  cjmulrcl  11069  reim0bd  11126  rerebd  11127  cjrebd  11128  caucvgre  11163  cvg1nlemcxze  11164  cvg1nlemcau  11166  cvg1nlemres  11167  recvguniq  11177  resqrexlemover  11192  resqrexlemdec  11193  resqrexlemgt0  11202  resqrexlemoverl  11203  resqrexlemglsq  11204  rersqrtthlem  11212  sqrtgt0  11216  leabs  11256  absexpzap  11262  absle  11271  recvalap  11279  abstri  11286  abs2dif  11288  amgm2  11300  absne0d  11369  maxleim  11387  maxabslemab  11388  maxabslemlub  11389  maxltsup  11400  zmaxcl  11406  fimaxre2  11409  minmax  11412  rpmincl  11420  bdtrilem  11421  bdtri  11422  xrmaxleim  11426  xrmaxiflemcom  11431  xrmaxltsup  11440  xrmaxadd  11443  xrminmax  11447  xrminrpcl  11456  climconst  11472  climuni  11475  2clim  11483  climcn1  11490  climcn2  11491  reccn2ap  11495  climge0  11507  climle  11516  climsqz  11517  climsqz2  11518  serf0  11534  summodclem3  11562  summodclem2a  11563  fsumcl2lem  11580  sumpr  11595  sumtp  11596  fsum0diaglem  11622  mptfzshft  11624  fsumle  11645  fsumlt  11646  divcnv  11679  trireciplem  11682  expcnvap0  11684  expcnv  11686  explecnv  11687  geosergap  11688  cvgratnnlembern  11705  cvgratnnlemabsle  11709  cvgratnnlemsumlt  11710  cvgratz  11714  cvgratgt0  11715  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  clim2divap  11722  prodmodclem3  11757  prodmodclem2a  11758  fprodseq  11765  fprodmul  11773  fprodfac  11797  fprodconst  11802  fprodap0  11803  fprodap0f  11818  fprodle  11822  eftcl  11836  ef0lem  11842  efsub  11863  eftlub  11872  eflegeo  11883  tanval2ap  11895  sinadd  11918  cos2t  11932  cos2tsin  11933  sin01bnd  11939  cos01bnd  11940  eirraplem  11959  dvdsval2  11972  dvdsdc  11980  dvds0lem  11983  zdvdsdc  11994  dvdscmulr  12002  dvdsmulcr  12003  fsumdvds  12024  dvdslelemd  12025  divconjdvds  12031  dvdsext  12037  fzm1ndvds  12038  dvdsmod  12044  3dvds  12046  oexpneg  12059  2tp1odd  12066  mulsucdiv2z  12067  2teven  12069  zeo5  12070  opeo  12079  omeo  12080  nn0ob  12090  divalglemnqt  12102  bitsdc  12129  bits0o  12132  bitsfzolem  12136  bitsfzo  12137  bitsmod  12138  bitscmp  12140  bitsinv1lem  12143  gcddvds  12155  dvdslegcd  12156  gcdneg  12174  bezoutlemnewy  12188  bezoutlemstep  12189  bezoutlema  12191  bezoutlemb  12192  bezoutlemmo  12198  bezoutlemle  12200  bezoutlemsup  12201  dfgcd3  12202  bezout  12203  dfgcd2  12206  uzwodc  12229  lcmcllem  12260  lcmneg  12267  lcmgcdlem  12270  lcmdvds  12272  lcmid  12273  3lcm2e6woprm  12279  6lcm4e12  12280  ncoprmgcdne1b  12282  mulgcddvds  12287  divgcdcoprmex  12295  cncongr1  12296  cncongr2  12297  isprm2lem  12309  prmind2  12313  dvdsnprmd  12318  prm2orodd  12319  sqnprm  12329  isprm5lem  12334  rpexp  12346  sqrt2irrlem  12354  oddpwdclemdc  12366  sqrt2irraplemnn  12372  qnumdencoprm  12386  qeqnumdivden  12387  nn0gcdsq  12393  nn0sqrtelqelz  12399  nonsq  12400  phicl2  12407  phibnd  12410  hashdvds  12414  phiprmpw  12415  phimullem  12418  eulerthlemrprm  12422  eulerthlema  12423  eulerthlemth  12425  prmdiveq  12429  hashgcdlem  12431  odzdvds  12439  modprminv  12443  nnnn0modprm0  12449  modprmn0modprm0  12450  pythagtriplem10  12463  pythagtriplem19  12476  pythagtrip  12477  pcpre1  12486  pcpremul  12487  pceu  12489  pcmul  12495  pcdiv  12496  pcqmul  12497  pcqdiv  12501  pcexp  12503  pcdvdsb  12514  pcidlem  12517  pcdvdstr  12521  pcgcd1  12522  pc2dvds  12524  pcprmpw2  12527  difsqpwdvds  12532  pcaddlem  12533  pcadd  12534  pcadd2  12535  pcmpt  12537  pcmptdvds  12539  pcprod  12540  fldivp1  12542  pcfaclem  12543  pcfac  12544  pcbc  12545  qexpz  12546  pockthlem  12550  pockthg  12551  1arithlem4  12560  1arith  12561  1arith2  12562  4sqlem6  12577  4sqlem8  12579  4sqlem9  12580  4sqlem10  12581  4sqexercise1  12592  4sqexercise2  12593  4sqlemsdc  12594  4sqlem11  12595  4sqlem12  12596  4sqlem15  12599  4sqlem16  12600  4sqlem17  12601  znnen  12640  ennnfonelemk  12642  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemrnh  12658  ennnfonelemfun  12659  ennnfonelemf1  12660  ennnfonelemrn  12661  ennnfonelemnn0  12664  ctinfomlemom  12669  ctiunctlemudc  12679  unct  12684  omctfn  12685  ssnnctlemct  12688  nninfdclemp1  12692  nninfdc  12695  structfung  12720  setsfun  12738  setsfun0  12739  setscom  12743  strslfv3  12749  setsslid  12754  pwsdiagel  12999  pwssnf1o  13000  imasaddfnlemg  13016  imasaddvallemg  13017  mgmsscl  13063  plusffng  13067  mgmplusf  13068  mgm0  13071  mgm1  13072  opifismgmdc  13073  gsumfzval  13093  gsumprval  13101  sgrp1  13113  issgrpd  13114  prdsplusgsgrpcl  13116  mndpfo  13140  mndfo  13141  prdsplusgcl  13148  prdsidlem  13149  mnd1  13157  0subm  13186  mhmima  13193  grpinvfng  13246  isgrpinv  13256  grpinvid  13262  grpinvf1o  13272  grpinvadd  13280  grpsubf  13281  grpsubsub4  13295  grplactcnv  13304  grp1  13308  grp1inv  13309  prdsinvlem  13310  prdsinvgd  13312  qusgrp2  13319  mulgfng  13330  subginv  13387  resgrpisgrp  13401  subgintm  13404  0subg  13405  0nsg  13420  qusinv  13442  ghminv  13456  ghmrn  13463  ghmeql  13473  ghmnsgima  13474  kerf1ghm  13480  conjnmz  13485  rngass  13571  rngmneg1  13579  rngmneg2  13580  qusrng  13590  srgideu  13604  srgidmlem  13610  srgpcomp  13622  srg1expzeq1  13627  ringcl  13645  ringideu  13649  ringidmlem  13654  ringnegl  13683  ringnegr  13684  ring1  13691  qusring2  13698  opprringbg  13712  dvdsrd  13726  dvdsr01  13736  isunitd  13738  unitinvcl  13755  unitinvinv  13756  unitnegcl  13762  rhmmul  13796  rhmf1o  13800  nzrunit  13820  lringuplu  13828  subrngintm  13844  subrgsubm  13866  subrgintm  13875  aprsym  13916  scaffng  13941  lmodscaf  13942  lsssn0  14002  lss1d  14015  lssintclm  14016  lspval  14022  lspcl  14023  lspsnid  14039  lspprid1  14043  lspsn  14048  sraval  14069  rspcl  14123  rspssid  14124  rspssp  14126  rnglidlmmgm  14128  rnglidlmsgrp  14129  cnfldneg  14205  zringinvg  14236  expghmap  14239  znzrhfo  14280  znf1o  14283  znhash  14288  znidomb  14290  znrrg  14292  psraddcl  14308  psr0cl  14309  psrnegcl  14311  psrneg  14315  psr1clfi  14316  baspartn  14370  eltg3i  14376  tgclb  14385  topbas  14387  2basgeng  14402  topcld  14429  0cld  14432  uncld  14433  neif  14461  elnei  14472  0nei  14486  restbasg  14488  iscnp4  14538  cnpnei  14539  cnclima  14543  cncnp  14550  cnrest2r  14557  cndis  14561  lmff  14569  lmtopcnp  14570  txbas  14578  txopn  14585  txcnp  14591  upxp  14592  txdis1cn  14598  cnmpt11  14603  cnmpt21  14611  psmetge0  14651  xmetge0  14685  xmettpos  14690  xmetrtri  14696  metrtri  14697  xblpnfps  14718  xblpnf  14719  blfps  14729  blf  14730  ssblps  14745  ssbl  14746  blbas  14753  metss2  14818  xmettxlem  14829  xmettx  14830  qtopbas  14842  divcnap  14885  cncfss  14903  cdivcncfap  14924  expcncf  14929  cnopnap  14931  maxcncf  14935  mincncf  14936  dedekindeulemuub  14937  dedekindeulemlu  14941  dedekindeu  14943  suplociccex  14945  dedekindicclemuub  14946  dedekindicclemlu  14950  dedekindicclemicc  14952  ivthinclemlopn  14956  ivthinclemuopn  14958  ivthinc  14963  ivthreinc  14965  hoverlt1  14969  ellimc3apf  14980  limcimolemlt  14984  limcimo  14985  limcresi  14986  cnplimclemle  14988  reldvg  14999  dvfgg  15008  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvcjbr  15028  dvcj  15029  dvrecap  15033  dveflem  15046  dvef  15047  elply2  15055  elplyr  15060  plycj  15081  plyreres  15084  reeff1oleme  15092  pilem3  15103  sinq34lt0t  15151  cosq14gt0  15152  coseq0q4123  15154  tangtx  15158  sincosq1eq  15159  cosordlem  15169  logdivlti  15201  relogbval  15271  relogbzcl  15272  nnlogbexp  15279  logbgcd1irr  15287  logbgcd1irraplemexp  15288  logbgcd1irraplemap  15289  wilthlem1  15300  mpodvdsmulf1o  15310  mersenne  15317  perfectlem2  15320  perfect  15321  zabsle1  15324  lgslem1  15325  lgsval  15329  lgsfvalg  15330  lgsfcl2  15331  lgsval2lem  15335  lgscl1  15348  lgsmod  15351  lgsdir2lem5  15357  lgsdir2  15358  lgsdilem2  15361  lgsdi  15362  lgsne0  15363  gausslemma2dlem0c  15376  gausslemma2dlem0h  15381  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  gausslemma2dlem3  15388  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgseisen  15399  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad3  15409  2lgslem3b1  15423  2lgslem3c1  15424  2lgs  15429  2lgsoddprmlem2  15431  2lgsoddprm  15438  2sqlem3  15442  2sqlem8  15448  2sqlem10  15450  fnmptd  15534  bj-sels  15644  bj-nnelon  15689  2omap  15726  pwle2  15729  pwf1oexmid  15730  pw1nct  15734  nninfall  15740  nninfsellemdc  15741  nninfself  15744  refeq  15759  isomninnlem  15761  cvgcmp2nlemabs  15763  trilpolemlt1  15772  trirec0  15775  apdifflemf  15777  apdifflemr  15778  apdiff  15779  iswomninnlem  15780  iswomni0  15782  ismkvnnlem  15783  reap0  15789  cndcap  15790