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  696  mpbir2and  934  pm3.12dc  948  mpbir3and  1170  pm5.15dc  1379  eqeltrd  2243  eqnetrd  2360  3netr4d  2369  r19.30dc  2613  sbcne12g  3063  eqsstrd  3178  3sstr4d  3187  eqbrtrd  4004  3brtr4d  4014  snelpwi  4190  prelpwi  4192  pwel  4196  ordelon  4361  onin  4364  elelsuc  4387  suceloni  4478  sucelon  4480  onintonm  4494  omsinds  4599  sosng  4677  relssdv  4696  eqbrrdv  4701  eqrelrdv2  4703  relsnopg  4708  breldmg  4810  elrnmptdv  4858  iss  4930  xpimasn  5052  elxp4  5091  elxp5  5092  funssres  5230  f0rn0  5382  sefvex  5507  fvun1  5552  eqfnfvd  5586  fvimacnvi  5599  fvimacnv  5600  fvelrn  5616  fmpt3d  5641  fmpt2d  5647  resflem  5649  fmptco  5651  fsn  5657  ftpg  5669  fconst2g  5700  funfvima3  5718  foeqcnvco  5758  f1eqcocnv  5759  fliftfun  5764  fliftfund  5765  fliftval  5768  riota5f  5822  f1ofveu  5830  f1ocnvd  6040  f1opw2  6044  off  6062  offval2  6065  ofrfval2  6066  caofref  6071  caofinvl  6072  elxp6  6137  cnvf1olem  6192  f2ndf  6194  f1od2  6203  tposf12  6237  smores2  6262  tfrlemisucaccv  6293  tfrlemibfn  6296  tfr1onlemsucaccv  6309  tfr1onlembfn  6312  tfrcllemsucaccv  6322  tfrcllembfn  6325  tfrcl  6332  tfri3  6335  frecabcl  6367  nnsucsssuc  6460  ersym  6513  ertr  6516  swoer  6529  erth  6545  riinerm  6574  qliftfund  6584  eroprf  6594  ecopoverg  6602  th3qlem1  6603  elmapssres  6639  mapss  6657  fdiagfn  6658  ixpssmap2g  6693  mapsnf1o  6703  f1dom2g  6722  dom3d  6740  fopwdom  6802  mapxpen  6814  nndomo  6830  dif1en  6845  findcard2  6855  findcard2s  6856  diffisn  6859  fimax2gtrilemstep  6866  fientri3  6880  fiintim  6894  f1dmvrnfibi  6909  sbthlemi6  6927  elfir  6938  fifo  6945  supelti  6967  supsnti  6970  cnvinfex  6983  ordiso2  7000  updjud  7047  djudom  7058  difinfsn  7065  ctssdc  7078  enumctlemm  7079  enumct  7080  enomnilem  7102  fodjuf  7109  ismkvnex  7119  omnimkv  7120  enmkvlem  7125  enwomnilem  7133  isnumi  7138  exmidfodomrlemrALT  7159  djudoml  7175  djudomr  7176  cc2lem  7207  cc3  7209  ltsopi  7261  pitri3or  7263  ltdcpi  7264  indpi  7283  enqdc  7302  enqdc1  7303  addcmpblnq  7308  mulcanenq  7326  recrecnq  7335  nqtri3or  7337  ltdcnq  7338  ltsonq  7339  ltaddnq  7348  subhalfnqq  7355  archnqq  7358  prarloclemarch2  7360  enq0tr  7375  nqnq0  7382  addcmpblnq0  7384  mulcanenq0ec  7386  nnnq0lem1  7387  nqpnq0nq  7394  nq0m0r  7397  nq02m  7406  prarloclemlt  7434  prarloclemcalc  7443  addlocpr  7477  nqprl  7492  nqpru  7493  addnqprlemrl  7498  addnqprlemru  7499  prmuloclemcalc  7506  mullocprlem  7511  mulnqprlemrl  7514  mulnqprlemru  7515  1idprl  7531  1idpru  7532  ltaddpr  7538  ltexprlemm  7541  ltexprlemopl  7542  ltexprlemopu  7544  ltexprlemdisj  7547  ltexprlemrl  7551  ltexprlemru  7553  addcanprleml  7555  addcanprlemu  7556  addcanprg  7557  prplnqu  7561  recexprlemloc  7572  recexprlem1ssl  7574  recexprlem1ssu  7575  aptiprleml  7580  aptiprlemu  7581  archpr  7584  cauappcvgprlemm  7586  cauappcvgprlemopl  7587  cauappcvgprlemloc  7593  cauappcvgprlemladdfu  7595  cauappcvgprlemladdfl  7596  cauappcvgprlem1  7600  cauappcvgprlem2  7601  caucvgprlemnkj  7607  caucvgprlemopl  7610  caucvgprlemloc  7616  caucvgprlemladdfu  7618  caucvgprlem2  7621  caucvgprprlemnkltj  7630  caucvgprprlemopl  7638  caucvgprprlemloc  7644  caucvgprprlemexbt  7647  caucvgprprlemaddq  7649  caucvgprprlem2  7651  suplocexprlemmu  7659  suplocexprlemru  7660  suplocexprlemloc  7662  suplocexprlemlub  7665  prsrlem1  7683  0idsr  7708  1idsr  7709  recexgt0sr  7714  archsr  7723  prsradd  7727  caucvgsrlemcau  7734  caucvgsrlembound  7735  caucvgsrlemoffgt1  7740  suplocsrlemb  7747  suplocsrlempr  7748  suplocsrlem  7749  pitonnlem1p1  7787  pitonn  7789  pitoregt0  7790  peano2nnnn  7794  recidpirq  7799  axcaucvglemval  7838  leid  7982  nltled  8019  readdcan  8038  addneintrd  8086  addneintr2d  8087  pncan  8104  subsub2  8126  subsub4  8131  negned  8206  subne0d  8218  subneintrd  8253  subneintr2d  8255  subeq0bd  8277  subdi  8283  gt0add  8471  rimul  8483  rereim  8484  ltmul1a  8489  apreim  8501  apirr  8503  mulap0r  8513  msqge0  8514  mulge0  8517  gt0ap0  8524  ltap  8531  subap0d  8542  recexaplem2  8549  mulap0bad  8556  mulap0bbd  8557  mul0eqap  8567  divrecap  8584  div0ap  8598  div1  8599  recrecap  8605  divdivdivap  8609  ddcanap  8622  rerecclap  8626  div2negap  8631  diveqap1bd  8732  recgt0  8745  prodgt0  8747  lemul1a  8753  recp1lt1  8794  squeeze0  8799  peano2nn  8869  div4p1lem1div2  9110  arch  9111  peano2z  9227  peano2zm  9229  ztri3or  9234  nn0n0n1ge2  9261  zextle  9282  gtndiv  9286  suprzclex  9289  nn0ind-raph  9308  uzid  9480  uzneg  9484  uztric  9487  uz11  9488  eluzp1l  9490  qdivcl  9581  irrmul  9585  rpnegap  9622  negelrpd  9624  ledivge1le  9662  mul2lt0rlt0  9695  mul2lt0rgt0  9696  nn0ledivnn  9703  ltpnf  9716  mnflt  9719  pnfge  9725  mnfle  9728  xrlttr  9731  xrltso  9732  xrlttri3  9733  xrleid  9736  xaddass2  9806  xltadd1  9812  xlt2add  9816  xleaddadd  9823  iccf1o  9940  fztri3or  9974  fznlem  9976  fzn  9977  fzsplit2  9985  fznatpl1  10011  uzsplit  10027  fseq1p1m1  10029  fzm1  10035  fznn0sub2  10063  difelfznle  10070  1fv  10074  fzodcel  10087  fzospliti  10111  fzouzsplit  10114  eluzgtdifelfzo  10132  exfzdc  10175  subfzo0  10177  exbtwnz  10186  qbtwnrelemcalc  10191  flqlelt  10211  qfraclt1  10215  qfracge0  10216  flqltnz  10222  btwnzge0  10235  flhalf  10237  ceiqle  10248  intfracq  10255  mulqmod0  10265  modqge0  10267  modqlt  10268  modqid  10284  modqid0  10285  m1modge3gt1  10306  modqltm1p1mod  10311  q2txmodxeq0  10319  modaddmodlo  10323  modsumfzodifsn  10331  addmodlteq  10333  frecuzrdgtcl  10347  frecuzrdgtclt  10356  uzennn  10371  uzsinds  10377  seqf  10396  seqf2  10399  monoord2  10412  iseqf1olemqk  10429  iseqf1olemjpcl  10430  iseqf1olemqpcl  10431  seq3f1olemqsumkj  10433  seq3f1olemqsum  10435  seq3f1olemstep  10436  seq3f1oleml  10438  ser3le  10453  exp3vallem  10456  exp3val  10457  expp1  10462  expcllem  10466  ltexp2a  10507  leexp2a  10508  nn0ltexp2  10623  faclbnd  10654  faclbnd2  10655  faclbnd3  10656  bcval5  10676  bcpasc  10679  hashennn  10693  fihasheqf1oi  10701  hashsng  10711  fihashfn  10713  hashun  10718  fihashss  10729  fihashssdif  10731  hashfz  10734  hashxp  10739  fimaxq  10740  zfz1isolem1  10753  seq3coll  10755  shftfn  10766  cjth  10788  cjmulrcl  10829  reim0bd  10886  rerebd  10887  cjrebd  10888  caucvgre  10923  cvg1nlemcxze  10924  cvg1nlemcau  10926  cvg1nlemres  10927  recvguniq  10937  resqrexlemover  10952  resqrexlemdec  10953  resqrexlemgt0  10962  resqrexlemoverl  10963  resqrexlemglsq  10964  rersqrtthlem  10972  sqrtgt0  10976  leabs  11016  absexpzap  11022  absle  11031  recvalap  11039  abstri  11046  abs2dif  11048  amgm2  11060  absne0d  11129  maxleim  11147  maxabslemab  11148  maxabslemlub  11149  maxltsup  11160  zmaxcl  11166  fimaxre2  11168  minmax  11171  rpmincl  11179  bdtrilem  11180  bdtri  11181  xrmaxleim  11185  xrmaxiflemcom  11190  xrmaxltsup  11199  xrmaxadd  11202  xrminmax  11206  xrminrpcl  11215  climconst  11231  climuni  11234  2clim  11242  climcn1  11249  climcn2  11250  reccn2ap  11254  climge0  11266  climle  11275  climsqz  11276  climsqz2  11277  serf0  11293  summodclem3  11321  summodclem2a  11322  fsumcl2lem  11339  sumpr  11354  sumtp  11355  fsum0diaglem  11381  mptfzshft  11383  fsumle  11404  fsumlt  11405  divcnv  11438  trireciplem  11441  expcnvap0  11443  expcnv  11445  explecnv  11446  geosergap  11447  cvgratnnlembern  11464  cvgratnnlemabsle  11468  cvgratnnlemsumlt  11469  cvgratz  11473  cvgratgt0  11474  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  clim2divap  11481  prodmodclem3  11516  prodmodclem2a  11517  fprodseq  11524  fprodmul  11532  fprodfac  11556  fprodconst  11561  fprodap0  11562  fprodap0f  11577  fprodle  11581  eftcl  11595  ef0lem  11601  efsub  11622  eftlub  11631  eflegeo  11642  tanval2ap  11654  sinadd  11677  cos2t  11691  cos2tsin  11692  sin01bnd  11698  cos01bnd  11699  eirraplem  11717  dvdsval2  11730  dvdsdc  11738  dvds0lem  11741  zdvdsdc  11752  dvdscmulr  11760  dvdsmulcr  11761  dvdslelemd  11781  divconjdvds  11787  dvdsext  11793  fzm1ndvds  11794  dvdsmod  11800  oexpneg  11814  2tp1odd  11821  mulsucdiv2z  11822  2teven  11824  zeo5  11825  opeo  11834  omeo  11835  nn0ob  11845  divalglemnqt  11857  zsupcllemstep  11878  zsupcl  11880  zssinfcl  11881  infssuzex  11882  infssuzcldc  11884  suprzubdc  11885  nninfdcex  11886  gcddvds  11896  dvdslegcd  11897  gcdneg  11915  bezoutlemnewy  11929  bezoutlemstep  11930  bezoutlema  11932  bezoutlemb  11933  bezoutlemmo  11939  bezoutlemle  11941  bezoutlemsup  11942  dfgcd3  11943  bezout  11944  dfgcd2  11947  uzwodc  11970  lcmcllem  11999  lcmneg  12006  lcmgcdlem  12009  lcmdvds  12011  lcmid  12012  3lcm2e6woprm  12018  6lcm4e12  12019  ncoprmgcdne1b  12021  mulgcddvds  12026  divgcdcoprmex  12034  cncongr1  12035  cncongr2  12036  isprm2lem  12048  prmind2  12052  dvdsnprmd  12057  prm2orodd  12058  sqnprm  12068  isprm5lem  12073  rpexp  12085  sqrt2irrlem  12093  oddpwdclemdc  12105  sqrt2irraplemnn  12111  qnumdencoprm  12125  qeqnumdivden  12126  nn0gcdsq  12132  nn0sqrtelqelz  12138  nonsq  12139  phicl2  12146  phibnd  12149  hashdvds  12153  phiprmpw  12154  phimullem  12157  eulerthlemrprm  12161  eulerthlema  12162  eulerthlemth  12164  prmdiveq  12168  hashgcdlem  12170  odzdvds  12177  modprminv  12181  nnnn0modprm0  12187  modprmn0modprm0  12188  pythagtriplem10  12201  pythagtriplem19  12214  pythagtrip  12215  pcpre1  12224  pcpremul  12225  pceu  12227  pcmul  12233  pcdiv  12234  pcqmul  12235  pcqdiv  12239  pcexp  12241  pcdvdsb  12251  pcidlem  12254  pcdvdstr  12258  pcgcd1  12259  pc2dvds  12261  pcprmpw2  12264  difsqpwdvds  12269  pcaddlem  12270  pcadd  12271  pcmpt  12273  pcmptdvds  12275  pcprod  12276  fldivp1  12278  pcfaclem  12279  pcfac  12280  pcbc  12281  qexpz  12282  pockthlem  12286  pockthg  12287  1arithlem4  12296  1arith  12297  1arith2  12298  4sqlem6  12313  4sqlem8  12315  4sqlem9  12316  4sqlem10  12317  znnen  12331  ennnfonelemk  12333  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ennnfonelemrnh  12349  ennnfonelemfun  12350  ennnfonelemf1  12351  ennnfonelemrn  12352  ennnfonelemnn0  12355  ctinfomlemom  12360  ctiunctlemudc  12370  unct  12375  omctfn  12376  ssnnctlemct  12379  nninfdclemp1  12383  nninfdc  12386  structfung  12411  setsfun  12429  setsfun0  12430  setscom  12434  setsslid  12444  mgmsscl  12592  plusffng  12596  mgmplusf  12597  mgm0  12600  mgm1  12601  opifismgmdc  12602  sgrp1  12628  baspartn  12698  eltg3i  12706  tgclb  12715  topbas  12717  2basgeng  12732  topcld  12759  0cld  12762  uncld  12763  neif  12791  elnei  12802  0nei  12816  restbasg  12818  iscnp4  12868  cnpnei  12869  cnclima  12873  cncnp  12880  cnrest2r  12887  cndis  12891  lmff  12899  lmtopcnp  12900  txbas  12908  txopn  12915  txcnp  12921  upxp  12922  txdis1cn  12928  cnmpt11  12933  cnmpt21  12941  psmetge0  12981  xmetge0  13015  xmettpos  13020  xmetrtri  13026  metrtri  13027  xblpnfps  13048  xblpnf  13049  blfps  13059  blf  13060  ssblps  13075  ssbl  13076  blbas  13083  metss2  13148  xmettxlem  13159  xmettx  13160  qtopbas  13172  divcnap  13205  cncfss  13220  cdivcncfap  13237  expcncf  13242  cnopnap  13244  dedekindeulemuub  13245  dedekindeulemlu  13249  dedekindeu  13251  suplociccex  13253  dedekindicclemuub  13254  dedekindicclemlu  13258  dedekindicclemicc  13260  ivthinclemlopn  13264  ivthinclemuopn  13266  ivthinc  13271  ellimc3apf  13279  limcimolemlt  13283  limcimo  13284  limcresi  13285  cnplimclemle  13287  reldvg  13298  dvfgg  13307  dvidlemap  13310  dvcjbr  13322  dvcj  13323  dvrecap  13327  dveflem  13337  dvef  13338  reeff1oleme  13343  pilem3  13354  sinq34lt0t  13402  cosq14gt0  13403  coseq0q4123  13405  tangtx  13409  sincosq1eq  13410  cosordlem  13420  logdivlti  13452  relogbval  13519  relogbzcl  13520  nnlogbexp  13527  logbgcd1irr  13535  logbgcd1irraplemexp  13536  logbgcd1irraplemap  13537  zabsle1  13550  lgslem1  13551  lgsval  13555  lgsfvalg  13556  lgsfcl2  13557  lgsval2lem  13561  lgscl1  13574  lgsmod  13577  lgsdir2lem5  13583  lgsdir2  13584  lgsdilem2  13587  lgsdi  13588  lgsne0  13589  2sqlem3  13603  2sqlem8  13609  2sqlem10  13611  fnmptd  13696  bj-sels  13806  bj-nnelon  13851  pwle2  13888  pwf1oexmid  13889  pw1nct  13893  nninfall  13899  nninfsellemdc  13900  nninfself  13903  refeq  13917  isomninnlem  13919  cvgcmp2nlemabs  13921  trilpolemlt1  13930  trirec0  13933  apdifflemf  13935  apdifflemr  13936  apdiff  13937  iswomninnlem  13938  iswomni0  13940  ismkvnnlem  13941  reap0  13947