Theorem mpbird 166

Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpbird.min	⊢ (𝜑 → 𝜒)
mpbird.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbird	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbird

Step	Hyp	Ref	Expression
1		mpbird.min	. 2 ⊢ (𝜑 → 𝜒)
2		mpbird.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimprd 157	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝜓)

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  929  pm3.12dc  943  mpbir3and  1165  pm5.15dc  1368  eqeltrd  2217  eqnetrd  2333  3netr4d  2342  sbcne12g  3025  eqsstrd  3138  3sstr4d  3147  eqbrtrd  3958  3brtr4d  3968  snelpwi  4142  prelpwi  4144  pwel  4148  ordelon  4313  onin  4316  elelsuc  4339  suceloni  4425  sucelon  4427  onintonm  4441  omsinds  4543  sosng  4620  relssdv  4639  eqbrrdv  4644  eqrelrdv2  4646  relsnopg  4651  breldmg  4753  elrnmptdv  4801  iss  4873  xpimasn  4995  elxp4  5034  elxp5  5035  funssres  5173  f0rn0  5325  sefvex  5450  fvun1  5495  eqfnfvd  5529  fvimacnvi  5542  fvimacnv  5543  fvelrn  5559  fmpt3d  5584  fmpt2d  5590  resflem  5592  fmptco  5594  fsn  5600  ftpg  5612  fconst2g  5643  funfvima3  5659  foeqcnvco  5699  f1eqcocnv  5700  fliftfun  5705  fliftfund  5706  fliftval  5709  riota5f  5762  f1ofveu  5770  f1ocnvd  5980  f1opw2  5984  off  6002  offval2  6005  ofrfval2  6006  caofref  6011  caofinvl  6012  elxp6  6075  cnvf1olem  6129  f2ndf  6131  f1od2  6140  tposf12  6174  smores2  6199  tfrlemisucaccv  6230  tfrlemibfn  6233  tfr1onlemsucaccv  6246  tfr1onlembfn  6249  tfrcllemsucaccv  6259  tfrcllembfn  6262  tfrcl  6269  tfri3  6272  frecabcl  6304  nnsucsssuc  6396  ersym  6449  ertr  6452  swoer  6465  erth  6481  riinerm  6510  qliftfund  6520  eroprf  6530  ecopoverg  6538  th3qlem1  6539  elmapssres  6575  mapss  6593  fdiagfn  6594  ixpssmap2g  6629  mapsnf1o  6639  f1dom2g  6658  dom3d  6676  fopwdom  6738  mapxpen  6750  nndomo  6766  dif1en  6781  findcard2  6791  findcard2s  6792  diffisn  6795  fimax2gtrilemstep  6802  fientri3  6811  fiintim  6825  f1dmvrnfibi  6840  sbthlemi6  6858  elfir  6869  fifo  6876  supelti  6897  supsnti  6900  cnvinfex  6913  ordiso2  6928  updjud  6975  djudom  6986  difinfsn  6993  ctssdc  7006  enumctlemm  7007  enumct  7008  enomnilem  7018  fodjuf  7025  ismkvnex  7037  omnimkv  7038  enmkvlem  7043  enwomnilem  7050  isnumi  7055  exmidfodomrlemrALT  7076  djudoml  7092  djudomr  7093  cc2lem  7098  cc3  7100  ltsopi  7152  pitri3or  7154  ltdcpi  7155  indpi  7174  enqdc  7193  enqdc1  7194  addcmpblnq  7199  mulcanenq  7217  recrecnq  7226  nqtri3or  7228  ltdcnq  7229  ltsonq  7230  ltaddnq  7239  subhalfnqq  7246  archnqq  7249  prarloclemarch2  7251  enq0tr  7266  nqnq0  7273  addcmpblnq0  7275  mulcanenq0ec  7277  nnnq0lem1  7278  nqpnq0nq  7285  nq0m0r  7288  nq02m  7297  prarloclemlt  7325  prarloclemcalc  7334  addlocpr  7368  nqprl  7383  nqpru  7384  addnqprlemrl  7389  addnqprlemru  7390  prmuloclemcalc  7397  mullocprlem  7402  mulnqprlemrl  7405  mulnqprlemru  7406  1idprl  7422  1idpru  7423  ltaddpr  7429  ltexprlemm  7432  ltexprlemopl  7433  ltexprlemopu  7435  ltexprlemdisj  7438  ltexprlemrl  7442  ltexprlemru  7444  addcanprleml  7446  addcanprlemu  7447  addcanprg  7448  prplnqu  7452  recexprlemloc  7463  recexprlem1ssl  7465  recexprlem1ssu  7466  aptiprleml  7471  aptiprlemu  7472  archpr  7475  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemloc  7484  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  cauappcvgprlem1  7491  cauappcvgprlem2  7492  caucvgprlemnkj  7498  caucvgprlemopl  7501  caucvgprlemloc  7507  caucvgprlemladdfu  7509  caucvgprlem2  7512  caucvgprprlemnkltj  7521  caucvgprprlemopl  7529  caucvgprprlemloc  7535  caucvgprprlemexbt  7538  caucvgprprlemaddq  7540  caucvgprprlem2  7542  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemloc  7553  suplocexprlemlub  7556  prsrlem1  7574  0idsr  7599  1idsr  7600  recexgt0sr  7605  archsr  7614  prsradd  7618  caucvgsrlemcau  7625  caucvgsrlembound  7626  caucvgsrlemoffgt1  7631  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  pitonnlem1p1  7678  pitonn  7680  pitoregt0  7681  peano2nnnn  7685  recidpirq  7690  axcaucvglemval  7729  leid  7872  nltled  7907  readdcan  7926  addneintrd  7974  addneintr2d  7975  pncan  7992  subsub2  8014  subsub4  8019  negned  8094  subne0d  8106  subneintrd  8141  subneintr2d  8143  subeq0bd  8165  subdi  8171  gt0add  8359  rimul  8371  rereim  8372  ltmul1a  8377  apreim  8389  apirr  8391  mulap0r  8401  msqge0  8402  mulge0  8405  gt0ap0  8412  ltap  8419  recexaplem2  8437  mulap0bad  8444  mulap0bbd  8445  mul0eqap  8455  divrecap  8472  div0ap  8486  div1  8487  recrecap  8493  divdivdivap  8497  ddcanap  8510  rerecclap  8514  div2negap  8519  diveqap1bd  8619  recgt0  8632  prodgt0  8634  lemul1a  8640  recp1lt1  8681  squeeze0  8686  peano2nn  8756  div4p1lem1div2  8997  arch  8998  peano2z  9114  peano2zm  9116  ztri3or  9121  nn0n0n1ge2  9145  zextle  9166  gtndiv  9170  suprzclex  9173  nn0ind-raph  9192  uzid  9364  uzneg  9368  uztric  9371  uz11  9372  eluzp1l  9374  qdivcl  9462  irrmul  9466  rpnegap  9503  negelrpd  9505  ledivge1le  9543  mul2lt0rlt0  9576  mul2lt0rgt0  9577  nn0ledivnn  9584  ltpnf  9597  mnflt  9599  pnfge  9605  mnfle  9608  xrlttr  9611  xrltso  9612  xrlttri3  9613  xrleid  9616  xaddass2  9683  xltadd1  9689  xlt2add  9693  xleaddadd  9700  iccf1o  9817  fztri3or  9850  fznlem  9852  fzn  9853  fzsplit2  9861  fznatpl1  9887  uzsplit  9903  fseq1p1m1  9905  fzm1  9911  fznn0sub2  9936  difelfznle  9943  1fv  9947  fzodcel  9960  fzospliti  9984  fzouzsplit  9987  eluzgtdifelfzo  10005  exfzdc  10048  subfzo0  10050  exbtwnz  10059  qbtwnrelemcalc  10064  flqlelt  10080  qfraclt1  10084  qfracge0  10085  flqltnz  10091  btwnzge0  10104  flhalf  10106  ceiqle  10117  intfracq  10124  mulqmod0  10134  modqge0  10136  modqlt  10137  modqid  10153  modqid0  10154  m1modge3gt1  10175  modqltm1p1mod  10180  q2txmodxeq0  10188  modaddmodlo  10192  modsumfzodifsn  10200  addmodlteq  10202  frecuzrdgtcl  10216  frecuzrdgtclt  10225  uzennn  10240  uzsinds  10246  seqf  10265  seqf2  10268  monoord2  10281  iseqf1olemqk  10298  iseqf1olemjpcl  10299  iseqf1olemqpcl  10300  seq3f1olemqsumkj  10302  seq3f1olemqsum  10304  seq3f1olemstep  10305  seq3f1oleml  10307  ser3le  10322  exp3vallem  10325  exp3val  10326  expp1  10331  expcllem  10335  ltexp2a  10376  leexp2a  10377  faclbnd  10519  faclbnd2  10520  faclbnd3  10521  bcval5  10541  bcpasc  10544  hashennn  10558  fihasheqf1oi  10566  hashsng  10576  fihashfn  10578  hashun  10583  fihashss  10594  fihashssdif  10596  hashfz  10599  hashxp  10604  fimaxq  10605  zfz1isolem1  10615  seq3coll  10617  shftfn  10628  cjth  10650  cjmulrcl  10691  reim0bd  10748  rerebd  10749  cjrebd  10750  caucvgre  10785  cvg1nlemcxze  10786  cvg1nlemcau  10788  cvg1nlemres  10789  recvguniq  10799  resqrexlemover  10814  resqrexlemdec  10815  resqrexlemgt0  10824  resqrexlemoverl  10825  resqrexlemglsq  10826  rersqrtthlem  10834  sqrtgt0  10838  leabs  10878  absexpzap  10884  absle  10893  recvalap  10901  abstri  10908  abs2dif  10910  amgm2  10922  absne0d  10991  maxleim  11009  maxabslemab  11010  maxabslemlub  11011  maxltsup  11022  zmaxcl  11028  fimaxre2  11030  minmax  11033  rpmincl  11041  bdtrilem  11042  bdtri  11043  xrmaxleim  11045  xrmaxiflemcom  11050  xrmaxltsup  11059  xrmaxadd  11062  xrminmax  11066  xrminrpcl  11075  climconst  11091  climuni  11094  2clim  11102  climcn1  11109  climcn2  11110  reccn2ap  11114  climge0  11126  climle  11135  climsqz  11136  climsqz2  11137  serf0  11153  summodclem3  11181  summodclem2a  11182  fsumcl2lem  11199  sumpr  11214  sumtp  11215  fsum0diaglem  11241  mptfzshft  11243  fsumle  11264  fsumlt  11265  divcnv  11298  trireciplem  11301  expcnvap0  11303  expcnv  11305  explecnv  11306  geosergap  11307  cvgratnnlembern  11324  cvgratnnlemabsle  11328  cvgratnnlemsumlt  11329  cvgratz  11333  cvgratgt0  11334  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  clim2divap  11341  prodmodclem3  11376  prodmodclem2a  11377  fprodseq  11384  eftcl  11397  ef0lem  11403  efsub  11424  eftlub  11433  eflegeo  11444  tanval2ap  11456  sinadd  11479  cos2t  11493  cos2tsin  11494  sin01bnd  11500  cos01bnd  11501  eirraplem  11519  dvdsval2  11532  dvdsdc  11537  dvds0lem  11539  zdvdsdc  11550  dvdscmulr  11558  dvdsmulcr  11559  dvdslelemd  11577  divconjdvds  11583  dvdsext  11589  fzm1ndvds  11590  dvdsmod  11596  oexpneg  11610  2tp1odd  11617  mulsucdiv2z  11618  2teven  11620  zeo5  11621  opeo  11630  omeo  11631  nn0ob  11641  divalglemnqt  11653  zsupcllemstep  11674  zsupcl  11676  zssinfcl  11677  infssuzex  11678  infssuzcldc  11680  gcddvds  11688  dvdslegcd  11689  gcdneg  11706  bezoutlemnewy  11720  bezoutlemstep  11721  bezoutlema  11723  bezoutlemb  11724  bezoutlemmo  11730  bezoutlemle  11732  bezoutlemsup  11733  dfgcd3  11734  bezout  11735  dfgcd2  11738  lcmcllem  11784  lcmneg  11791  lcmgcdlem  11794  lcmdvds  11796  lcmid  11797  3lcm2e6woprm  11803  6lcm4e12  11804  ncoprmgcdne1b  11806  mulgcddvds  11811  divgcdcoprmex  11819  cncongr1  11820  cncongr2  11821  isprm2lem  11833  prmind2  11837  dvdsnprmd  11842  prm2orodd  11843  sqnprm  11852  rpexp  11867  sqrt2irrlem  11875  oddpwdclemdc  11887  sqrt2irraplemnn  11893  qnumdencoprm  11907  qeqnumdivden  11908  nn0gcdsq  11914  nn0sqrtelqelz  11920  nonsq  11921  phicl2  11926  phibnd  11929  hashdvds  11933  phiprmpw  11934  phimullem  11937  hashgcdlem  11939  znnen  11947  ennnfonelemk  11949  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemrnh  11965  ennnfonelemfun  11966  ennnfonelemf1  11967  ennnfonelemrn  11968  ennnfonelemnn0  11971  ctinfomlemom  11976  ctiunctlemudc  11986  unct  11991  omctfn  11992  structfung  12015  setsfun  12033  setsfun0  12034  setscom  12038  setsslid  12048  baspartn  12256  eltg3i  12264  tgclb  12273  topbas  12275  2basgeng  12290  topcld  12317  0cld  12320  uncld  12321  neif  12349  elnei  12360  0nei  12374  restbasg  12376  iscnp4  12426  cnpnei  12427  cnclima  12431  cncnp  12438  cnrest2r  12445  cndis  12449  lmff  12457  lmtopcnp  12458  txbas  12466  txopn  12473  txcnp  12479  upxp  12480  txdis1cn  12486  cnmpt11  12491  cnmpt21  12499  psmetge0  12539  xmetge0  12573  xmettpos  12578  xmetrtri  12584  metrtri  12585  xblpnfps  12606  xblpnf  12607  blfps  12617  blf  12618  ssblps  12633  ssbl  12634  blbas  12641  metss2  12706  xmettxlem  12717  xmettx  12718  qtopbas  12730  divcnap  12763  cncfss  12778  cdivcncfap  12795  expcncf  12800  cnopnap  12802  dedekindeulemuub  12803  dedekindeulemlu  12807  dedekindeu  12809  suplociccex  12811  dedekindicclemuub  12812  dedekindicclemlu  12816  dedekindicclemicc  12818  ivthinclemlopn  12822  ivthinclemuopn  12824  ivthinc  12829  ellimc3apf  12837  limcimolemlt  12841  limcimo  12842  limcresi  12843  cnplimclemle  12845  reldvg  12856  dvfgg  12865  dvidlemap  12868  dvcjbr  12880  dvcj  12881  dvrecap  12885  dveflem  12895  dvef  12896  reeff1oleme  12901  pilem3  12912  sinq34lt0t  12960  cosq14gt0  12961  coseq0q4123  12963  tangtx  12967  sincosq1eq  12968  cosordlem  12978  logdivlti  13010  relogbval  13076  relogbzcl  13077  nnlogbexp  13084  logbgcd1irr  13092  logbgcd1irraplemexp  13093  logbgcd1irraplemap  13094  bj-sels  13283  bj-nnelon  13328  pwle2  13366  pwf1oexmid  13367  pw1nct  13371  nninfall  13379  nninfsellemdc  13381  nninfself  13384  refeq  13398  isomninnlem  13400  cvgcmp2nlemabs  13402  trilpolemlt1  13409  trirec0  13412  apdifflemf  13414  apdifflemr  13415  apdiff  13416  iswomninnlem  13417  ismkvnnlem  13419