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  933  pm3.12dc  947  mpbir3and  1169  pm5.15dc  1378  eqeltrd  2241  eqnetrd  2358  3netr4d  2367  r19.30dc  2611  sbcne12g  3058  eqsstrd  3173  3sstr4d  3182  eqbrtrd  3998  3brtr4d  4008  snelpwi  4184  prelpwi  4186  pwel  4190  ordelon  4355  onin  4358  elelsuc  4381  suceloni  4472  sucelon  4474  onintonm  4488  omsinds  4593  sosng  4671  relssdv  4690  eqbrrdv  4695  eqrelrdv2  4697  relsnopg  4702  breldmg  4804  elrnmptdv  4852  iss  4924  xpimasn  5046  elxp4  5085  elxp5  5086  funssres  5224  f0rn0  5376  sefvex  5501  fvun1  5546  eqfnfvd  5580  fvimacnvi  5593  fvimacnv  5594  fvelrn  5610  fmpt3d  5635  fmpt2d  5641  resflem  5643  fmptco  5645  fsn  5651  ftpg  5663  fconst2g  5694  funfvima3  5712  foeqcnvco  5752  f1eqcocnv  5753  fliftfun  5758  fliftfund  5759  fliftval  5762  riota5f  5816  f1ofveu  5824  f1ocnvd  6034  f1opw2  6038  off  6056  offval2  6059  ofrfval2  6060  caofref  6065  caofinvl  6066  elxp6  6129  cnvf1olem  6183  f2ndf  6185  f1od2  6194  tposf12  6228  smores2  6253  tfrlemisucaccv  6284  tfrlemibfn  6287  tfr1onlemsucaccv  6300  tfr1onlembfn  6303  tfrcllemsucaccv  6313  tfrcllembfn  6316  tfrcl  6323  tfri3  6326  frecabcl  6358  nnsucsssuc  6451  ersym  6504  ertr  6507  swoer  6520  erth  6536  riinerm  6565  qliftfund  6575  eroprf  6585  ecopoverg  6593  th3qlem1  6594  elmapssres  6630  mapss  6648  fdiagfn  6649  ixpssmap2g  6684  mapsnf1o  6694  f1dom2g  6713  dom3d  6731  fopwdom  6793  mapxpen  6805  nndomo  6821  dif1en  6836  findcard2  6846  findcard2s  6847  diffisn  6850  fimax2gtrilemstep  6857  fientri3  6871  fiintim  6885  f1dmvrnfibi  6900  sbthlemi6  6918  elfir  6929  fifo  6936  supelti  6958  supsnti  6961  cnvinfex  6974  ordiso2  6991  updjud  7038  djudom  7049  difinfsn  7056  ctssdc  7069  enumctlemm  7070  enumct  7071  enomnilem  7093  fodjuf  7100  ismkvnex  7110  omnimkv  7111  enmkvlem  7116  enwomnilem  7124  isnumi  7129  exmidfodomrlemrALT  7150  djudoml  7166  djudomr  7167  cc2lem  7198  cc3  7200  ltsopi  7252  pitri3or  7254  ltdcpi  7255  indpi  7274  enqdc  7293  enqdc1  7294  addcmpblnq  7299  mulcanenq  7317  recrecnq  7326  nqtri3or  7328  ltdcnq  7329  ltsonq  7330  ltaddnq  7339  subhalfnqq  7346  archnqq  7349  prarloclemarch2  7351  enq0tr  7366  nqnq0  7373  addcmpblnq0  7375  mulcanenq0ec  7377  nnnq0lem1  7378  nqpnq0nq  7385  nq0m0r  7388  nq02m  7397  prarloclemlt  7425  prarloclemcalc  7434  addlocpr  7468  nqprl  7483  nqpru  7484  addnqprlemrl  7489  addnqprlemru  7490  prmuloclemcalc  7497  mullocprlem  7502  mulnqprlemrl  7505  mulnqprlemru  7506  1idprl  7522  1idpru  7523  ltaddpr  7529  ltexprlemm  7532  ltexprlemopl  7533  ltexprlemopu  7535  ltexprlemdisj  7538  ltexprlemrl  7542  ltexprlemru  7544  addcanprleml  7546  addcanprlemu  7547  addcanprg  7548  prplnqu  7552  recexprlemloc  7563  recexprlem1ssl  7565  recexprlem1ssu  7566  aptiprleml  7571  aptiprlemu  7572  archpr  7575  cauappcvgprlemm  7577  cauappcvgprlemopl  7578  cauappcvgprlemloc  7584  cauappcvgprlemladdfu  7586  cauappcvgprlemladdfl  7587  cauappcvgprlem1  7591  cauappcvgprlem2  7592  caucvgprlemnkj  7598  caucvgprlemopl  7601  caucvgprlemloc  7607  caucvgprlemladdfu  7609  caucvgprlem2  7612  caucvgprprlemnkltj  7621  caucvgprprlemopl  7629  caucvgprprlemloc  7635  caucvgprprlemexbt  7638  caucvgprprlemaddq  7640  caucvgprprlem2  7642  suplocexprlemmu  7650  suplocexprlemru  7651  suplocexprlemloc  7653  suplocexprlemlub  7656  prsrlem1  7674  0idsr  7699  1idsr  7700  recexgt0sr  7705  archsr  7714  prsradd  7718  caucvgsrlemcau  7725  caucvgsrlembound  7726  caucvgsrlemoffgt1  7731  suplocsrlemb  7738  suplocsrlempr  7739  suplocsrlem  7740  pitonnlem1p1  7778  pitonn  7780  pitoregt0  7781  peano2nnnn  7785  recidpirq  7790  axcaucvglemval  7829  leid  7973  nltled  8010  readdcan  8029  addneintrd  8077  addneintr2d  8078  pncan  8095  subsub2  8117  subsub4  8122  negned  8197  subne0d  8209  subneintrd  8244  subneintr2d  8246  subeq0bd  8268  subdi  8274  gt0add  8462  rimul  8474  rereim  8475  ltmul1a  8480  apreim  8492  apirr  8494  mulap0r  8504  msqge0  8505  mulge0  8508  gt0ap0  8515  ltap  8522  subap0d  8533  recexaplem2  8540  mulap0bad  8547  mulap0bbd  8548  mul0eqap  8558  divrecap  8575  div0ap  8589  div1  8590  recrecap  8596  divdivdivap  8600  ddcanap  8613  rerecclap  8617  div2negap  8622  diveqap1bd  8723  recgt0  8736  prodgt0  8738  lemul1a  8744  recp1lt1  8785  squeeze0  8790  peano2nn  8860  div4p1lem1div2  9101  arch  9102  peano2z  9218  peano2zm  9220  ztri3or  9225  nn0n0n1ge2  9252  zextle  9273  gtndiv  9277  suprzclex  9280  nn0ind-raph  9299  uzid  9471  uzneg  9475  uztric  9478  uz11  9479  eluzp1l  9481  qdivcl  9572  irrmul  9576  rpnegap  9613  negelrpd  9615  ledivge1le  9653  mul2lt0rlt0  9686  mul2lt0rgt0  9687  nn0ledivnn  9694  ltpnf  9707  mnflt  9710  pnfge  9716  mnfle  9719  xrlttr  9722  xrltso  9723  xrlttri3  9724  xrleid  9727  xaddass2  9797  xltadd1  9803  xlt2add  9807  xleaddadd  9814  iccf1o  9931  fztri3or  9964  fznlem  9966  fzn  9967  fzsplit2  9975  fznatpl1  10001  uzsplit  10017  fseq1p1m1  10019  fzm1  10025  fznn0sub2  10053  difelfznle  10060  1fv  10064  fzodcel  10077  fzospliti  10101  fzouzsplit  10104  eluzgtdifelfzo  10122  exfzdc  10165  subfzo0  10167  exbtwnz  10176  qbtwnrelemcalc  10181  flqlelt  10201  qfraclt1  10205  qfracge0  10206  flqltnz  10212  btwnzge0  10225  flhalf  10227  ceiqle  10238  intfracq  10245  mulqmod0  10255  modqge0  10257  modqlt  10258  modqid  10274  modqid0  10275  m1modge3gt1  10296  modqltm1p1mod  10301  q2txmodxeq0  10309  modaddmodlo  10313  modsumfzodifsn  10321  addmodlteq  10323  frecuzrdgtcl  10337  frecuzrdgtclt  10346  uzennn  10361  uzsinds  10367  seqf  10386  seqf2  10389  monoord2  10402  iseqf1olemqk  10419  iseqf1olemjpcl  10420  iseqf1olemqpcl  10421  seq3f1olemqsumkj  10423  seq3f1olemqsum  10425  seq3f1olemstep  10426  seq3f1oleml  10428  ser3le  10443  exp3vallem  10446  exp3val  10447  expp1  10452  expcllem  10456  ltexp2a  10497  leexp2a  10498  nn0ltexp2  10612  faclbnd  10643  faclbnd2  10644  faclbnd3  10645  bcval5  10665  bcpasc  10668  hashennn  10682  fihasheqf1oi  10690  hashsng  10700  fihashfn  10702  hashun  10707  fihashss  10718  fihashssdif  10720  hashfz  10723  hashxp  10728  fimaxq  10729  zfz1isolem1  10739  seq3coll  10741  shftfn  10752  cjth  10774  cjmulrcl  10815  reim0bd  10872  rerebd  10873  cjrebd  10874  caucvgre  10909  cvg1nlemcxze  10910  cvg1nlemcau  10912  cvg1nlemres  10913  recvguniq  10923  resqrexlemover  10938  resqrexlemdec  10939  resqrexlemgt0  10948  resqrexlemoverl  10949  resqrexlemglsq  10950  rersqrtthlem  10958  sqrtgt0  10962  leabs  11002  absexpzap  11008  absle  11017  recvalap  11025  abstri  11032  abs2dif  11034  amgm2  11046  absne0d  11115  maxleim  11133  maxabslemab  11134  maxabslemlub  11135  maxltsup  11146  zmaxcl  11152  fimaxre2  11154  minmax  11157  rpmincl  11165  bdtrilem  11166  bdtri  11167  xrmaxleim  11171  xrmaxiflemcom  11176  xrmaxltsup  11185  xrmaxadd  11188  xrminmax  11192  xrminrpcl  11201  climconst  11217  climuni  11220  2clim  11228  climcn1  11235  climcn2  11236  reccn2ap  11240  climge0  11252  climle  11261  climsqz  11262  climsqz2  11263  serf0  11279  summodclem3  11307  summodclem2a  11308  fsumcl2lem  11325  sumpr  11340  sumtp  11341  fsum0diaglem  11367  mptfzshft  11369  fsumle  11390  fsumlt  11391  divcnv  11424  trireciplem  11427  expcnvap0  11429  expcnv  11431  explecnv  11432  geosergap  11433  cvgratnnlembern  11450  cvgratnnlemabsle  11454  cvgratnnlemsumlt  11455  cvgratz  11459  cvgratgt0  11460  mertenslemi1  11462  mertenslem2  11463  mertensabs  11464  clim2divap  11467  prodmodclem3  11502  prodmodclem2a  11503  fprodseq  11510  fprodmul  11518  fprodfac  11542  fprodconst  11547  fprodap0  11548  fprodap0f  11563  fprodle  11567  eftcl  11581  ef0lem  11587  efsub  11608  eftlub  11617  eflegeo  11628  tanval2ap  11640  sinadd  11663  cos2t  11677  cos2tsin  11678  sin01bnd  11684  cos01bnd  11685  eirraplem  11703  dvdsval2  11716  dvdsdc  11724  dvds0lem  11727  zdvdsdc  11738  dvdscmulr  11746  dvdsmulcr  11747  dvdslelemd  11766  divconjdvds  11772  dvdsext  11778  fzm1ndvds  11779  dvdsmod  11785  oexpneg  11799  2tp1odd  11806  mulsucdiv2z  11807  2teven  11809  zeo5  11810  opeo  11819  omeo  11820  nn0ob  11830  divalglemnqt  11842  zsupcllemstep  11863  zsupcl  11865  zssinfcl  11866  infssuzex  11867  infssuzcldc  11869  suprzubdc  11870  nninfdcex  11871  gcddvds  11881  dvdslegcd  11882  gcdneg  11900  bezoutlemnewy  11914  bezoutlemstep  11915  bezoutlema  11917  bezoutlemb  11918  bezoutlemmo  11924  bezoutlemle  11926  bezoutlemsup  11927  dfgcd3  11928  bezout  11929  dfgcd2  11932  lcmcllem  11978  lcmneg  11985  lcmgcdlem  11988  lcmdvds  11990  lcmid  11991  3lcm2e6woprm  11997  6lcm4e12  11998  ncoprmgcdne1b  12000  mulgcddvds  12005  divgcdcoprmex  12013  cncongr1  12014  cncongr2  12015  isprm2lem  12027  prmind2  12031  dvdsnprmd  12036  prm2orodd  12037  sqnprm  12047  rpexp  12062  sqrt2irrlem  12070  oddpwdclemdc  12082  sqrt2irraplemnn  12088  qnumdencoprm  12102  qeqnumdivden  12103  nn0gcdsq  12109  nn0sqrtelqelz  12115  nonsq  12116  phicl2  12123  phibnd  12126  hashdvds  12130  phiprmpw  12131  phimullem  12134  eulerthlemrprm  12138  eulerthlema  12139  eulerthlemth  12141  prmdiveq  12145  hashgcdlem  12147  odzdvds  12154  modprminv  12158  nnnn0modprm0  12164  modprmn0modprm0  12165  pythagtriplem10  12178  pythagtriplem19  12191  pythagtrip  12192  pcpre1  12201  pcpremul  12202  pceu  12204  pcmul  12210  pcdiv  12211  pcqmul  12212  pcqdiv  12216  pcexp  12218  pcdvdsb  12228  pcidlem  12231  pcdvdstr  12235  pcgcd1  12236  pc2dvds  12238  pcprmpw2  12241  difsqpwdvds  12246  pcaddlem  12247  pcadd  12248  pcmpt  12250  pcmptdvds  12252  pcprod  12253  fldivp1  12255  pcfaclem  12256  pcfac  12257  pcbc  12258  qexpz  12259  znnen  12268  ennnfonelemk  12270  ennnfonelemkh  12282  ennnfonelemhf1o  12283  ennnfonelemrnh  12286  ennnfonelemfun  12287  ennnfonelemf1  12288  ennnfonelemrn  12289  ennnfonelemnn0  12292  ctinfomlemom  12297  ctiunctlemudc  12307  unct  12312  omctfn  12313  ssnnctlemct  12316  nninfdclemp1  12322  nninfdc  12325  structfung  12348  setsfun  12366  setsfun0  12367  setscom  12371  setsslid  12381  baspartn  12589  eltg3i  12597  tgclb  12606  topbas  12608  2basgeng  12623  topcld  12650  0cld  12653  uncld  12654  neif  12682  elnei  12693  0nei  12707  restbasg  12709  iscnp4  12759  cnpnei  12760  cnclima  12764  cncnp  12771  cnrest2r  12778  cndis  12782  lmff  12790  lmtopcnp  12791  txbas  12799  txopn  12806  txcnp  12812  upxp  12813  txdis1cn  12819  cnmpt11  12824  cnmpt21  12832  psmetge0  12872  xmetge0  12906  xmettpos  12911  xmetrtri  12917  metrtri  12918  xblpnfps  12939  xblpnf  12940  blfps  12950  blf  12951  ssblps  12966  ssbl  12967  blbas  12974  metss2  13039  xmettxlem  13050  xmettx  13051  qtopbas  13063  divcnap  13096  cncfss  13111  cdivcncfap  13128  expcncf  13133  cnopnap  13135  dedekindeulemuub  13136  dedekindeulemlu  13140  dedekindeu  13142  suplociccex  13144  dedekindicclemuub  13145  dedekindicclemlu  13149  dedekindicclemicc  13151  ivthinclemlopn  13155  ivthinclemuopn  13157  ivthinc  13162  ellimc3apf  13170  limcimolemlt  13174  limcimo  13175  limcresi  13176  cnplimclemle  13178  reldvg  13189  dvfgg  13198  dvidlemap  13201  dvcjbr  13213  dvcj  13214  dvrecap  13218  dveflem  13228  dvef  13229  reeff1oleme  13234  pilem3  13245  sinq34lt0t  13293  cosq14gt0  13294  coseq0q4123  13296  tangtx  13300  sincosq1eq  13301  cosordlem  13311  logdivlti  13343  relogbval  13410  relogbzcl  13411  nnlogbexp  13418  logbgcd1irr  13426  logbgcd1irraplemexp  13427  logbgcd1irraplemap  13428  fnmptd  13521  bj-sels  13631  bj-nnelon  13676  pwle2  13712  pwf1oexmid  13713  pw1nct  13717  nninfall  13723  nninfsellemdc  13724  nninfself  13727  refeq  13741  isomninnlem  13743  cvgcmp2nlemabs  13745  trilpolemlt1  13754  trirec0  13757  apdifflemf  13759  apdifflemr  13760  apdiff  13761  iswomninnlem  13762  iswomni0  13764  ismkvnnlem  13765  reap0  13771