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  2270  eqnetrd  2388  3netr4d  2397  r19.30dc  2641  raleqtrrdv  2700  rexeqtrrdv  2701  sbcne12g  3099  eqsstrd  3216  3sstr4d  3225  eqbrtrd  4052  3brtr4d  4062  snelpwi  4242  prelpwi  4244  pwel  4248  ordelon  4415  onin  4418  elelsuc  4441  onsuc  4534  onsucb  4536  onintonm  4550  omsinds  4655  sosng  4733  relssdv  4752  eqbrrdv  4757  eqrelrdv2  4759  relsnopg  4764  breldmg  4869  elrnmptdv  4917  iss  4989  xpimasn  5115  elxp4  5154  elxp5  5155  iotam  5247  funssres  5297  f0rn0  5449  fimadmfo  5486  sefvex  5576  fvun1  5624  eqfnfvd  5659  fvimacnvi  5673  fvimacnv  5674  fvelrn  5690  fmpt3d  5715  fmpt2d  5721  resflem  5723  fmptco  5725  fsn  5731  ftpg  5743  fconst2g  5774  funfvima3  5793  elabrexg  5802  foeqcnvco  5834  f1eqcocnv  5835  fliftfun  5840  fliftfund  5841  fliftval  5844  riota5f  5899  f1ofveu  5907  f1ocnvd  6122  f1opw2  6126  off  6145  offval2  6148  ofrfval2  6149  caofref  6156  caofinvl  6157  elxp6  6224  cnvf1olem  6279  f2ndf  6281  f1od2  6290  tposf12  6324  smores2  6349  tfrlemisucaccv  6380  tfrlemibfn  6383  tfr1onlemsucaccv  6396  tfr1onlembfn  6399  tfrcllemsucaccv  6409  tfrcllembfn  6412  tfrcl  6419  tfri3  6422  frecabcl  6454  nnsucsssuc  6547  ersym  6601  ertr  6604  swoer  6617  erth  6635  riinerm  6664  qliftfund  6674  eroprf  6684  ecopoverg  6692  th3qlem1  6693  elmapssres  6729  mapss  6747  fdiagfn  6748  ixpssmap2g  6783  mapsnf1o  6793  f1dom2g  6812  dom3d  6830  pw2f1odclem  6892  fopwdom  6894  mapxpen  6906  nndomo  6922  dif1en  6937  findcard2  6947  findcard2s  6948  diffisn  6951  fimax2gtrilemstep  6958  fientri3  6973  fiintim  6987  opabfi  6994  f1dmvrnfibi  7005  sbthlemi6  7023  elfir  7034  fifo  7041  supelti  7063  supsnti  7066  cnvinfex  7079  ordiso2  7096  updjud  7143  djudom  7154  difinfsn  7161  ctssdc  7174  enumctlemm  7175  enumct  7176  nninfninc  7184  enomnilem  7199  fodjuf  7206  ismkvnex  7216  omnimkv  7217  enmkvlem  7222  enwomnilem  7230  nninfdcinf  7232  nninfwlporlem  7234  isnumi  7244  exmidfodomrlemrALT  7265  djudoml  7281  djudomr  7282  netap  7316  2omotaplemap  7319  2omotaplemst  7320  exmidapne  7322  cc2lem  7328  cc3  7330  ltsopi  7382  pitri3or  7384  ltdcpi  7385  indpi  7404  enqdc  7423  enqdc1  7424  addcmpblnq  7429  mulcanenq  7447  recrecnq  7456  nqtri3or  7458  ltdcnq  7459  ltsonq  7460  ltaddnq  7469  subhalfnqq  7476  archnqq  7479  prarloclemarch2  7481  enq0tr  7496  nqnq0  7503  addcmpblnq0  7505  mulcanenq0ec  7507  nnnq0lem1  7508  nqpnq0nq  7515  nq0m0r  7518  nq02m  7527  prarloclemlt  7555  prarloclemcalc  7564  addlocpr  7598  nqprl  7613  nqpru  7614  addnqprlemrl  7619  addnqprlemru  7620  prmuloclemcalc  7627  mullocprlem  7632  mulnqprlemrl  7635  mulnqprlemru  7636  1idprl  7652  1idpru  7653  ltaddpr  7659  ltexprlemm  7662  ltexprlemopl  7663  ltexprlemopu  7665  ltexprlemdisj  7668  ltexprlemrl  7672  ltexprlemru  7674  addcanprleml  7676  addcanprlemu  7677  addcanprg  7678  prplnqu  7682  recexprlemloc  7693  recexprlem1ssl  7695  recexprlem1ssu  7696  aptiprleml  7701  aptiprlemu  7702  archpr  7705  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemloc  7714  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  cauappcvgprlem1  7721  cauappcvgprlem2  7722  caucvgprlemnkj  7728  caucvgprlemopl  7731  caucvgprlemloc  7737  caucvgprlemladdfu  7739  caucvgprlem2  7742  caucvgprprlemnkltj  7751  caucvgprprlemopl  7759  caucvgprprlemloc  7765  caucvgprprlemexbt  7768  caucvgprprlemaddq  7770  caucvgprprlem2  7772  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemloc  7783  suplocexprlemlub  7786  prsrlem1  7804  0idsr  7829  1idsr  7830  recexgt0sr  7835  archsr  7844  prsradd  7848  caucvgsrlemcau  7855  caucvgsrlembound  7856  caucvgsrlemoffgt1  7861  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  pitonnlem1p1  7908  pitonn  7910  pitoregt0  7911  peano2nnnn  7915  recidpirq  7920  axcaucvglemval  7959  leid  8105  nltled  8142  readdcan  8161  addneintrd  8209  addneintr2d  8210  pncan  8227  subsub2  8249  subsub4  8254  negned  8329  subne0d  8341  subneintrd  8376  subneintr2d  8378  subeq0bd  8400  subdi  8406  gt0add  8594  rimul  8606  rereim  8607  ltmul1a  8612  apreim  8624  apirr  8626  mulap0r  8636  msqge0  8637  mulge0  8640  gt0ap0  8647  ltap  8654  subap0d  8665  recexaplem2  8673  mulap0bad  8680  mulap0bbd  8681  mul0eqap  8691  divrecap  8709  div0ap  8723  div1  8724  recrecap  8730  divdivdivap  8734  ddcanap  8747  rerecclap  8751  div2negap  8756  diveqap1bd  8857  recgt0  8871  prodgt0  8873  lemul1a  8879  recp1lt1  8920  squeeze0  8925  peano2nn  8996  div4p1lem1div2  9239  arch  9240  peano2z  9356  peano2zm  9358  ztri3or  9363  nn0n0n1ge2  9390  zextle  9411  gtndiv  9415  suprzclex  9418  nn0ind-raph  9437  uzid  9609  uzneg  9614  uztric  9617  uz11  9618  eluzp1l  9620  qdivcl  9711  irrmul  9715  irrmulap  9716  rpnegap  9755  negelrpd  9757  ledivge1le  9795  mul2lt0rlt0  9828  mul2lt0rgt0  9829  nn0ledivnn  9836  ltpnf  9849  mnflt  9852  pnfge  9858  mnfle  9861  xrlttr  9864  xrltso  9865  xrlttri3  9866  xrleid  9869  xaddass2  9939  xltadd1  9945  xlt2add  9949  xleaddadd  9956  iccf1o  10073  fztri3or  10108  fznlem  10110  fzn  10111  fzsplit2  10119  fznatpl1  10145  uzsplit  10161  fseq1p1m1  10163  fzm1  10169  fznn0sub2  10197  difelfznle  10204  1fv  10208  fzodcel  10222  fzospliti  10246  fzouzsplit  10249  eluzgtdifelfzo  10267  exfzdc  10310  subfzo0  10312  exbtwnz  10322  qbtwnrelemcalc  10327  flqlelt  10348  qfraclt1  10352  qfracge0  10353  flqltnz  10359  btwnzge0  10372  flhalf  10374  fldiv4lem1div2uz2  10378  ceiqle  10387  intfracq  10394  mulqmod0  10404  modqge0  10406  modqlt  10407  modqid  10423  modqid0  10424  m1modge3gt1  10445  modqltm1p1mod  10450  q2txmodxeq0  10458  modaddmodlo  10462  modsumfzodifsn  10470  addmodlteq  10472  frecuzrdgtcl  10486  frecuzrdgtclt  10495  uzennn  10510  uzsinds  10518  seqf  10538  seqf2  10542  monoord2  10560  iseqf1olemqk  10581  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  seq3f1olemqsumkj  10585  seq3f1olemqsum  10587  seq3f1olemstep  10588  seq3f1oleml  10590  seqf1oglem1  10593  ser3le  10611  exp3vallem  10614  exp3val  10615  expp1  10620  expcllem  10624  ltexp2a  10665  leexp2a  10666  nn0ltexp2  10783  faclbnd  10815  faclbnd2  10816  faclbnd3  10817  bcval5  10837  bcpasc  10840  hashennn  10854  fihasheqf1oi  10861  hashsng  10872  fihashfn  10874  hashun  10879  fihashss  10890  fihashssdif  10892  hashfz  10895  hashxp  10900  fimaxq  10901  zfz1isolem1  10914  seq3coll  10916  wrdf  10923  wrdlenge2n0  10952  fstwrdne0  10956  wrdred1hash  10960  shftfn  10971  cjth  10993  cjmulrcl  11034  reim0bd  11091  rerebd  11092  cjrebd  11093  caucvgre  11128  cvg1nlemcxze  11129  cvg1nlemcau  11131  cvg1nlemres  11132  recvguniq  11142  resqrexlemover  11157  resqrexlemdec  11158  resqrexlemgt0  11167  resqrexlemoverl  11168  resqrexlemglsq  11169  rersqrtthlem  11177  sqrtgt0  11181  leabs  11221  absexpzap  11227  absle  11236  recvalap  11244  abstri  11251  abs2dif  11253  amgm2  11265  absne0d  11334  maxleim  11352  maxabslemab  11353  maxabslemlub  11354  maxltsup  11365  zmaxcl  11371  fimaxre2  11373  minmax  11376  rpmincl  11384  bdtrilem  11385  bdtri  11386  xrmaxleim  11390  xrmaxiflemcom  11395  xrmaxltsup  11404  xrmaxadd  11407  xrminmax  11411  xrminrpcl  11420  climconst  11436  climuni  11439  2clim  11447  climcn1  11454  climcn2  11455  reccn2ap  11459  climge0  11471  climle  11480  climsqz  11481  climsqz2  11482  serf0  11498  summodclem3  11526  summodclem2a  11527  fsumcl2lem  11544  sumpr  11559  sumtp  11560  fsum0diaglem  11586  mptfzshft  11588  fsumle  11609  fsumlt  11610  divcnv  11643  trireciplem  11646  expcnvap0  11648  expcnv  11650  explecnv  11651  geosergap  11652  cvgratnnlembern  11669  cvgratnnlemabsle  11673  cvgratnnlemsumlt  11674  cvgratz  11678  cvgratgt0  11679  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  clim2divap  11686  prodmodclem3  11721  prodmodclem2a  11722  fprodseq  11729  fprodmul  11737  fprodfac  11761  fprodconst  11766  fprodap0  11767  fprodap0f  11782  fprodle  11786  eftcl  11800  ef0lem  11806  efsub  11827  eftlub  11836  eflegeo  11847  tanval2ap  11859  sinadd  11882  cos2t  11896  cos2tsin  11897  sin01bnd  11903  cos01bnd  11904  eirraplem  11923  dvdsval2  11936  dvdsdc  11944  dvds0lem  11947  zdvdsdc  11958  dvdscmulr  11966  dvdsmulcr  11967  dvdslelemd  11988  divconjdvds  11994  dvdsext  12000  fzm1ndvds  12001  dvdsmod  12007  oexpneg  12021  2tp1odd  12028  mulsucdiv2z  12029  2teven  12031  zeo5  12032  opeo  12041  omeo  12042  nn0ob  12052  divalglemnqt  12064  zsupcllemstep  12085  zsupcl  12087  zssinfcl  12088  infssuzex  12089  infssuzcldc  12091  suprzubdc  12092  nninfdcex  12093  gcddvds  12103  dvdslegcd  12104  gcdneg  12122  bezoutlemnewy  12136  bezoutlemstep  12137  bezoutlema  12139  bezoutlemb  12140  bezoutlemmo  12146  bezoutlemle  12148  bezoutlemsup  12149  dfgcd3  12150  bezout  12151  dfgcd2  12154  uzwodc  12177  lcmcllem  12208  lcmneg  12215  lcmgcdlem  12218  lcmdvds  12220  lcmid  12221  3lcm2e6woprm  12227  6lcm4e12  12228  ncoprmgcdne1b  12230  mulgcddvds  12235  divgcdcoprmex  12243  cncongr1  12244  cncongr2  12245  isprm2lem  12257  prmind2  12261  dvdsnprmd  12266  prm2orodd  12267  sqnprm  12277  isprm5lem  12282  rpexp  12294  sqrt2irrlem  12302  oddpwdclemdc  12314  sqrt2irraplemnn  12320  qnumdencoprm  12334  qeqnumdivden  12335  nn0gcdsq  12341  nn0sqrtelqelz  12347  nonsq  12348  phicl2  12355  phibnd  12358  hashdvds  12362  phiprmpw  12363  phimullem  12366  eulerthlemrprm  12370  eulerthlema  12371  eulerthlemth  12373  prmdiveq  12377  hashgcdlem  12379  odzdvds  12386  modprminv  12390  nnnn0modprm0  12396  modprmn0modprm0  12397  pythagtriplem10  12410  pythagtriplem19  12423  pythagtrip  12424  pcpre1  12433  pcpremul  12434  pceu  12436  pcmul  12442  pcdiv  12443  pcqmul  12444  pcqdiv  12448  pcexp  12450  pcdvdsb  12461  pcidlem  12464  pcdvdstr  12468  pcgcd1  12469  pc2dvds  12471  pcprmpw2  12474  difsqpwdvds  12479  pcaddlem  12480  pcadd  12481  pcadd2  12482  pcmpt  12484  pcmptdvds  12486  pcprod  12487  fldivp1  12489  pcfaclem  12490  pcfac  12491  pcbc  12492  qexpz  12493  pockthlem  12497  pockthg  12498  1arithlem4  12507  1arith  12508  1arith2  12509  4sqlem6  12524  4sqlem8  12526  4sqlem9  12527  4sqlem10  12528  4sqexercise1  12539  4sqexercise2  12540  4sqlemsdc  12541  4sqlem11  12542  4sqlem12  12543  4sqlem15  12546  4sqlem16  12547  4sqlem17  12548  znnen  12558  ennnfonelemk  12560  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemrnh  12576  ennnfonelemfun  12577  ennnfonelemf1  12578  ennnfonelemrn  12579  ennnfonelemnn0  12582  ctinfomlemom  12587  ctiunctlemudc  12597  unct  12602  omctfn  12603  ssnnctlemct  12606  nninfdclemp1  12610  nninfdc  12613  structfung  12638  setsfun  12656  setsfun0  12657  setscom  12661  setsslid  12672  imasaddfnlemg  12900  imasaddvallemg  12901  mgmsscl  12947  plusffng  12951  mgmplusf  12952  mgm0  12955  mgm1  12956  opifismgmdc  12957  gsumfzval  12977  gsumprval  12985  sgrp1  12997  issgrpd  12998  mndpfo  13022  mndfo  13023  mnd1  13030  0subm  13059  mhmima  13066  grpinvfng  13119  isgrpinv  13129  grpinvid  13135  grpinvf1o  13145  grpinvadd  13153  grpsubf  13154  grpsubsub4  13168  grplactcnv  13177  grp1  13181  grp1inv  13182  qusgrp2  13186  mulgfng  13197  subginv  13254  resgrpisgrp  13268  subgintm  13271  0subg  13272  0nsg  13287  qusinv  13309  ghminv  13323  ghmrn  13330  ghmeql  13340  ghmnsgima  13341  kerf1ghm  13347  conjnmz  13352  rngass  13438  rngmneg1  13446  rngmneg2  13447  qusrng  13457  srgideu  13471  srgidmlem  13477  srgpcomp  13489  srg1expzeq1  13494  ringcl  13512  ringideu  13516  ringidmlem  13521  ringnegl  13550  ringnegr  13551  ring1  13558  qusring2  13565  opprringbg  13579  dvdsrd  13593  dvdsr01  13603  isunitd  13605  unitinvcl  13622  unitinvinv  13623  unitnegcl  13629  rhmmul  13663  rhmf1o  13667  nzrunit  13687  lringuplu  13695  subrngintm  13711  subrgsubm  13733  subrgintm  13742  aprsym  13783  scaffng  13808  lmodscaf  13809  lsssn0  13869  lss1d  13882  lssintclm  13883  lspval  13889  lspcl  13890  lspsnid  13906  lspprid1  13910  lspsn  13915  sraval  13936  rspcl  13990  rspssid  13991  rspssp  13993  rnglidlmmgm  13995  rnglidlmsgrp  13996  cnfldneg  14072  zringinvg  14103  expghmap  14106  znzrhfo  14147  znf1o  14150  znhash  14155  znidomb  14157  znrrg  14159  psraddcl  14175  baspartn  14229  eltg3i  14235  tgclb  14244  topbas  14246  2basgeng  14261  topcld  14288  0cld  14291  uncld  14292  neif  14320  elnei  14331  0nei  14345  restbasg  14347  iscnp4  14397  cnpnei  14398  cnclima  14402  cncnp  14409  cnrest2r  14416  cndis  14420  lmff  14428  lmtopcnp  14429  txbas  14437  txopn  14444  txcnp  14450  upxp  14451  txdis1cn  14457  cnmpt11  14462  cnmpt21  14470  psmetge0  14510  xmetge0  14544  xmettpos  14549  xmetrtri  14555  metrtri  14556  xblpnfps  14577  xblpnf  14578  blfps  14588  blf  14589  ssblps  14604  ssbl  14605  blbas  14612  metss2  14677  xmettxlem  14688  xmettx  14689  qtopbas  14701  divcnap  14744  cncfss  14762  cdivcncfap  14783  expcncf  14788  cnopnap  14790  maxcncf  14794  mincncf  14795  dedekindeulemuub  14796  dedekindeulemlu  14800  dedekindeu  14802  suplociccex  14804  dedekindicclemuub  14805  dedekindicclemlu  14809  dedekindicclemicc  14811  ivthinclemlopn  14815  ivthinclemuopn  14817  ivthinc  14822  ivthreinc  14824  hoverlt1  14828  ellimc3apf  14839  limcimolemlt  14843  limcimo  14844  limcresi  14845  cnplimclemle  14847  reldvg  14858  dvfgg  14867  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvcjbr  14887  dvcj  14888  dvrecap  14892  dveflem  14905  dvef  14906  elply2  14914  elplyr  14919  plycj  14939  plyreres  14942  reeff1oleme  14948  pilem3  14959  sinq34lt0t  15007  cosq14gt0  15008  coseq0q4123  15010  tangtx  15014  sincosq1eq  15015  cosordlem  15025  logdivlti  15057  relogbval  15124  relogbzcl  15125  nnlogbexp  15132  logbgcd1irr  15140  logbgcd1irraplemexp  15141  logbgcd1irraplemap  15142  wilthlem1  15153  zabsle1  15156  lgslem1  15157  lgsval  15161  lgsfvalg  15162  lgsfcl2  15163  lgsval2lem  15167  lgscl1  15180  lgsmod  15183  lgsdir2lem5  15189  lgsdir2  15190  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  gausslemma2dlem0c  15208  gausslemma2dlem0h  15213  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  gausslemma2dlem3  15220  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgseisen  15231  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad3  15241  2lgslem3b1  15255  2lgslem3c1  15256  2lgs  15261  2lgsoddprmlem2  15263  2lgsoddprm  15270  2sqlem3  15274  2sqlem8  15280  2sqlem10  15282  fnmptd  15366  bj-sels  15476  bj-nnelon  15521  pwle2  15559  pwf1oexmid  15560  pw1nct  15563  nninfall  15569  nninfsellemdc  15570  nninfself  15573  refeq  15588  isomninnlem  15590  cvgcmp2nlemabs  15592  trilpolemlt1  15601  trirec0  15604  apdifflemf  15606  apdifflemr  15607  apdiff  15608  iswomninnlem  15609  iswomni0  15611  ismkvnnlem  15612  reap0  15618  cndcap  15619