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  695  mpbir2and  928  pm3.12dc  942  mpbir3and  1164  pm5.15dc  1367  eqeltrd  2216  eqnetrd  2332  3netr4d  2341  sbcne12g  3020  eqsstrd  3133  3sstr4d  3142  eqbrtrd  3950  3brtr4d  3960  snelpwi  4134  prelpwi  4136  pwel  4140  ordelon  4305  onin  4308  elelsuc  4331  suceloni  4417  sucelon  4419  onintonm  4433  omsinds  4535  sosng  4612  relssdv  4631  eqbrrdv  4636  eqrelrdv2  4638  relsnopg  4643  breldmg  4745  elrnmptdv  4793  iss  4865  xpimasn  4987  elxp4  5026  elxp5  5027  funssres  5165  f0rn0  5317  sefvex  5442  fvun1  5487  eqfnfvd  5521  fvimacnvi  5534  fvimacnv  5535  fvelrn  5551  fmpt3d  5576  fmpt2d  5582  resflem  5584  fmptco  5586  fsn  5592  ftpg  5604  fconst2g  5635  funfvima3  5651  foeqcnvco  5691  f1eqcocnv  5692  fliftfun  5697  fliftfund  5698  fliftval  5701  riota5f  5754  f1ofveu  5762  f1ocnvd  5972  f1opw2  5976  off  5994  offval2  5997  ofrfval2  5998  caofref  6003  caofinvl  6004  elxp6  6067  cnvf1olem  6121  f2ndf  6123  f1od2  6132  tposf12  6166  smores2  6191  tfrlemisucaccv  6222  tfrlemibfn  6225  tfr1onlemsucaccv  6238  tfr1onlembfn  6241  tfrcllemsucaccv  6251  tfrcllembfn  6254  tfrcl  6261  tfri3  6264  frecabcl  6296  nnsucsssuc  6388  ersym  6441  ertr  6444  swoer  6457  erth  6473  riinerm  6502  qliftfund  6512  eroprf  6522  ecopoverg  6530  th3qlem1  6531  elmapssres  6567  mapss  6585  fdiagfn  6586  ixpssmap2g  6621  mapsnf1o  6631  f1dom2g  6650  dom3d  6668  fopwdom  6730  mapxpen  6742  nndomo  6758  dif1en  6773  findcard2  6783  findcard2s  6784  diffisn  6787  fimax2gtrilemstep  6794  fientri3  6803  fiintim  6817  f1dmvrnfibi  6832  sbthlemi6  6850  elfir  6861  fifo  6868  supelti  6889  supsnti  6892  cnvinfex  6905  ordiso2  6920  updjud  6967  djudom  6978  difinfsn  6985  ctssdc  6998  enumctlemm  6999  enumct  7000  enomnilem  7010  fodjuf  7017  ismkvnex  7029  omnimkv  7030  isnumi  7038  exmidfodomrlemrALT  7059  djudoml  7075  djudomr  7076  ltsopi  7128  pitri3or  7130  ltdcpi  7131  indpi  7150  enqdc  7169  enqdc1  7170  addcmpblnq  7175  mulcanenq  7193  recrecnq  7202  nqtri3or  7204  ltdcnq  7205  ltsonq  7206  ltaddnq  7215  subhalfnqq  7222  archnqq  7225  prarloclemarch2  7227  enq0tr  7242  nqnq0  7249  addcmpblnq0  7251  mulcanenq0ec  7253  nnnq0lem1  7254  nqpnq0nq  7261  nq0m0r  7264  nq02m  7273  prarloclemlt  7301  prarloclemcalc  7310  addlocpr  7344  nqprl  7359  nqpru  7360  addnqprlemrl  7365  addnqprlemru  7366  prmuloclemcalc  7373  mullocprlem  7378  mulnqprlemrl  7381  mulnqprlemru  7382  1idprl  7398  1idpru  7399  ltaddpr  7405  ltexprlemm  7408  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemdisj  7414  ltexprlemrl  7418  ltexprlemru  7420  addcanprleml  7422  addcanprlemu  7423  addcanprg  7424  prplnqu  7428  recexprlemloc  7439  recexprlem1ssl  7441  recexprlem1ssu  7442  aptiprleml  7447  aptiprlemu  7448  archpr  7451  cauappcvgprlemm  7453  cauappcvgprlemopl  7454  cauappcvgprlemloc  7460  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlem1  7467  cauappcvgprlem2  7468  caucvgprlemnkj  7474  caucvgprlemopl  7477  caucvgprlemloc  7483  caucvgprlemladdfu  7485  caucvgprlem2  7488  caucvgprprlemnkltj  7497  caucvgprprlemopl  7505  caucvgprprlemloc  7511  caucvgprprlemexbt  7514  caucvgprprlemaddq  7516  caucvgprprlem2  7518  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemloc  7529  suplocexprlemlub  7532  prsrlem1  7550  0idsr  7575  1idsr  7576  recexgt0sr  7581  archsr  7590  prsradd  7594  caucvgsrlemcau  7601  caucvgsrlembound  7602  caucvgsrlemoffgt1  7607  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  pitonnlem1p1  7654  pitonn  7656  pitoregt0  7657  peano2nnnn  7661  recidpirq  7666  axcaucvglemval  7705  leid  7848  nltled  7883  readdcan  7902  addneintrd  7950  addneintr2d  7951  pncan  7968  subsub2  7990  subsub4  7995  negned  8070  subne0d  8082  subneintrd  8117  subneintr2d  8119  subeq0bd  8141  subdi  8147  gt0add  8335  rimul  8347  rereim  8348  ltmul1a  8353  apreim  8365  apirr  8367  mulap0r  8377  msqge0  8378  mulge0  8381  gt0ap0  8388  ltap  8395  recexaplem2  8413  mulap0bad  8420  mulap0bbd  8421  mul0eqap  8431  divrecap  8448  div0ap  8462  div1  8463  recrecap  8469  divdivdivap  8473  ddcanap  8486  rerecclap  8490  div2negap  8495  diveqap1bd  8595  recgt0  8608  prodgt0  8610  lemul1a  8616  recp1lt1  8657  squeeze0  8662  peano2nn  8732  div4p1lem1div2  8973  arch  8974  peano2z  9090  peano2zm  9092  ztri3or  9097  nn0n0n1ge2  9121  zextle  9142  gtndiv  9146  suprzclex  9149  nn0ind-raph  9168  uzid  9340  uzneg  9344  uztric  9347  uz11  9348  eluzp1l  9350  qdivcl  9435  irrmul  9439  rpnegap  9474  negelrpd  9476  ledivge1le  9513  mul2lt0rlt0  9546  mul2lt0rgt0  9547  nn0ledivnn  9554  ltpnf  9567  mnflt  9569  pnfge  9575  mnfle  9578  xrlttr  9581  xrltso  9582  xrlttri3  9583  xrleid  9586  xaddass2  9653  xltadd1  9659  xlt2add  9663  xleaddadd  9670  iccf1o  9787  fztri3or  9819  fznlem  9821  fzn  9822  fzsplit2  9830  fznatpl1  9856  uzsplit  9872  fseq1p1m1  9874  fzm1  9880  fznn0sub2  9905  difelfznle  9912  1fv  9916  fzodcel  9929  fzospliti  9953  fzouzsplit  9956  eluzgtdifelfzo  9974  exfzdc  10017  subfzo0  10019  exbtwnz  10028  qbtwnrelemcalc  10033  flqlelt  10049  qfraclt1  10053  qfracge0  10054  flqltnz  10060  btwnzge0  10073  flhalf  10075  ceiqle  10086  intfracq  10093  mulqmod0  10103  modqge0  10105  modqlt  10106  modqid  10122  modqid0  10123  m1modge3gt1  10144  modqltm1p1mod  10149  q2txmodxeq0  10157  modaddmodlo  10161  modsumfzodifsn  10169  addmodlteq  10171  frecuzrdgtcl  10185  frecuzrdgtclt  10194  uzennn  10209  uzsinds  10215  seqf  10234  seqf2  10237  monoord2  10250  iseqf1olemqk  10267  iseqf1olemjpcl  10268  iseqf1olemqpcl  10269  seq3f1olemqsumkj  10271  seq3f1olemqsum  10273  seq3f1olemstep  10274  seq3f1oleml  10276  ser3le  10291  exp3vallem  10294  exp3val  10295  expp1  10300  expcllem  10304  ltexp2a  10345  leexp2a  10346  faclbnd  10487  faclbnd2  10488  faclbnd3  10489  bcval5  10509  bcpasc  10512  hashennn  10526  fihasheqf1oi  10534  hashsng  10544  fihashfn  10546  hashun  10551  fihashss  10562  fihashssdif  10564  hashfz  10567  hashxp  10572  fimaxq  10573  zfz1isolem1  10583  seq3coll  10585  shftfn  10596  cjth  10618  cjmulrcl  10659  reim0bd  10716  rerebd  10717  cjrebd  10718  caucvgre  10753  cvg1nlemcxze  10754  cvg1nlemcau  10756  cvg1nlemres  10757  recvguniq  10767  resqrexlemover  10782  resqrexlemdec  10783  resqrexlemgt0  10792  resqrexlemoverl  10793  resqrexlemglsq  10794  rersqrtthlem  10802  sqrtgt0  10806  leabs  10846  absexpzap  10852  absle  10861  recvalap  10869  abstri  10876  abs2dif  10878  amgm2  10890  absne0d  10959  maxleim  10977  maxabslemab  10978  maxabslemlub  10979  maxltsup  10990  zmaxcl  10996  fimaxre2  10998  minmax  11001  rpmincl  11009  bdtrilem  11010  bdtri  11011  xrmaxleim  11013  xrmaxiflemcom  11018  xrmaxltsup  11027  xrmaxadd  11030  xrminmax  11034  xrminrpcl  11043  climconst  11059  climuni  11062  2clim  11070  climcn1  11077  climcn2  11078  reccn2ap  11082  climge0  11094  climle  11103  climsqz  11104  climsqz2  11105  serf0  11121  summodclem3  11149  summodclem2a  11150  fsumcl2lem  11167  sumpr  11182  sumtp  11183  fsum0diaglem  11209  mptfzshft  11211  fsumle  11232  fsumlt  11233  divcnv  11266  trireciplem  11269  expcnvap0  11271  expcnv  11273  explecnv  11274  geosergap  11275  cvgratnnlembern  11292  cvgratnnlemabsle  11296  cvgratnnlemsumlt  11297  cvgratz  11301  cvgratgt0  11302  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  clim2divap  11309  prodmodclem3  11344  prodmodclem2a  11345  eftcl  11360  ef0lem  11366  efsub  11387  eftlub  11396  eflegeo  11408  tanval2ap  11420  sinadd  11443  cos2t  11457  cos2tsin  11458  sin01bnd  11464  cos01bnd  11465  eirraplem  11483  dvdsval2  11496  dvdsdc  11501  dvds0lem  11503  zdvdsdc  11514  dvdscmulr  11522  dvdsmulcr  11523  dvdslelemd  11541  divconjdvds  11547  dvdsext  11553  fzm1ndvds  11554  dvdsmod  11560  oexpneg  11574  2tp1odd  11581  mulsucdiv2z  11582  2teven  11584  zeo5  11585  opeo  11594  omeo  11595  nn0ob  11605  divalglemnqt  11617  zsupcllemstep  11638  zsupcl  11640  zssinfcl  11641  infssuzex  11642  infssuzcldc  11644  gcddvds  11652  dvdslegcd  11653  gcdneg  11670  bezoutlemnewy  11684  bezoutlemstep  11685  bezoutlema  11687  bezoutlemb  11688  bezoutlemmo  11694  bezoutlemle  11696  bezoutlemsup  11697  dfgcd3  11698  bezout  11699  dfgcd2  11702  lcmcllem  11748  lcmneg  11755  lcmgcdlem  11758  lcmdvds  11760  lcmid  11761  3lcm2e6woprm  11767  6lcm4e12  11768  ncoprmgcdne1b  11770  mulgcddvds  11775  divgcdcoprmex  11783  cncongr1  11784  cncongr2  11785  isprm2lem  11797  prmind2  11801  dvdsnprmd  11806  prm2orodd  11807  sqnprm  11816  rpexp  11831  sqrt2irrlem  11839  oddpwdclemdc  11851  sqrt2irraplemnn  11857  qnumdencoprm  11871  qeqnumdivden  11872  nn0gcdsq  11878  nn0sqrtelqelz  11884  nonsq  11885  phicl2  11890  phibnd  11893  hashdvds  11897  phiprmpw  11898  phimullem  11901  hashgcdlem  11903  znnen  11911  ennnfonelemk  11913  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemrnh  11929  ennnfonelemfun  11930  ennnfonelemf1  11931  ennnfonelemrn  11932  ennnfonelemnn0  11935  ctinfomlemom  11940  ctiunctlemudc  11950  unct  11954  structfung  11976  setsfun  11994  setsfun0  11995  setscom  11999  setsslid  12009  baspartn  12217  eltg3i  12225  tgclb  12234  topbas  12236  2basgeng  12251  topcld  12278  0cld  12281  uncld  12282  neif  12310  elnei  12321  0nei  12335  restbasg  12337  iscnp4  12387  cnpnei  12388  cnclima  12392  cncnp  12399  cnrest2r  12406  cndis  12410  lmff  12418  lmtopcnp  12419  txbas  12427  txopn  12434  txcnp  12440  upxp  12441  txdis1cn  12447  cnmpt11  12452  cnmpt21  12460  psmetge0  12500  xmetge0  12534  xmettpos  12539  xmetrtri  12545  metrtri  12546  xblpnfps  12567  xblpnf  12568  blfps  12578  blf  12579  ssblps  12594  ssbl  12595  blbas  12602  metss2  12667  xmettxlem  12678  xmettx  12679  qtopbas  12691  divcnap  12724  cncfss  12739  cdivcncfap  12756  expcncf  12761  cnopnap  12763  dedekindeulemuub  12764  dedekindeulemlu  12768  dedekindeu  12770  suplociccex  12772  dedekindicclemuub  12773  dedekindicclemlu  12777  dedekindicclemicc  12779  ivthinclemlopn  12783  ivthinclemuopn  12785  ivthinc  12790  ellimc3apf  12798  limcimolemlt  12802  limcimo  12803  limcresi  12804  cnplimclemle  12806  reldvg  12817  dvfgg  12826  dvidlemap  12829  dvcjbr  12841  dvcj  12842  dvrecap  12846  dveflem  12855  dvef  12856  pilem3  12864  sinq34lt0t  12912  cosq14gt0  12913  coseq0q4123  12915  tangtx  12919  sincosq1eq  12920  cosordlem  12930  bj-sels  13112  bj-nnelon  13157  pwle2  13193  pwf1oexmid  13194  nninfall  13204  nninfsellemdc  13206  nninfself  13209  refeq  13223  isomninnlem  13225  cvgcmp2nlemabs  13227  trilpolemlt1  13234