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  934  pm3.12dc  948  mpbir3and  1170  pm5.15dc  1379  eqeltrd  2242  eqnetrd  2359  3netr4d  2368  r19.30dc  2612  sbcne12g  3062  eqsstrd  3177  3sstr4d  3186  eqbrtrd  4003  3brtr4d  4013  snelpwi  4189  prelpwi  4191  pwel  4195  ordelon  4360  onin  4363  elelsuc  4386  suceloni  4477  sucelon  4479  onintonm  4493  omsinds  4598  sosng  4676  relssdv  4695  eqbrrdv  4700  eqrelrdv2  4702  relsnopg  4707  breldmg  4809  elrnmptdv  4857  iss  4929  xpimasn  5051  elxp4  5090  elxp5  5091  funssres  5229  f0rn0  5381  sefvex  5506  fvun1  5551  eqfnfvd  5585  fvimacnvi  5598  fvimacnv  5599  fvelrn  5615  fmpt3d  5640  fmpt2d  5646  resflem  5648  fmptco  5650  fsn  5656  ftpg  5668  fconst2g  5699  funfvima3  5717  foeqcnvco  5757  f1eqcocnv  5758  fliftfun  5763  fliftfund  5764  fliftval  5767  riota5f  5821  f1ofveu  5829  f1ocnvd  6039  f1opw2  6043  off  6061  offval2  6064  ofrfval2  6065  caofref  6070  caofinvl  6071  elxp6  6134  cnvf1olem  6188  f2ndf  6190  f1od2  6199  tposf12  6233  smores2  6258  tfrlemisucaccv  6289  tfrlemibfn  6292  tfr1onlemsucaccv  6305  tfr1onlembfn  6308  tfrcllemsucaccv  6318  tfrcllembfn  6321  tfrcl  6328  tfri3  6331  frecabcl  6363  nnsucsssuc  6456  ersym  6509  ertr  6512  swoer  6525  erth  6541  riinerm  6570  qliftfund  6580  eroprf  6590  ecopoverg  6598  th3qlem1  6599  elmapssres  6635  mapss  6653  fdiagfn  6654  ixpssmap2g  6689  mapsnf1o  6699  f1dom2g  6718  dom3d  6736  fopwdom  6798  mapxpen  6810  nndomo  6826  dif1en  6841  findcard2  6851  findcard2s  6852  diffisn  6855  fimax2gtrilemstep  6862  fientri3  6876  fiintim  6890  f1dmvrnfibi  6905  sbthlemi6  6923  elfir  6934  fifo  6941  supelti  6963  supsnti  6966  cnvinfex  6979  ordiso2  6996  updjud  7043  djudom  7054  difinfsn  7061  ctssdc  7074  enumctlemm  7075  enumct  7076  enomnilem  7098  fodjuf  7105  ismkvnex  7115  omnimkv  7116  enmkvlem  7121  enwomnilem  7129  isnumi  7134  exmidfodomrlemrALT  7155  djudoml  7171  djudomr  7172  cc2lem  7203  cc3  7205  ltsopi  7257  pitri3or  7259  ltdcpi  7260  indpi  7279  enqdc  7298  enqdc1  7299  addcmpblnq  7304  mulcanenq  7322  recrecnq  7331  nqtri3or  7333  ltdcnq  7334  ltsonq  7335  ltaddnq  7344  subhalfnqq  7351  archnqq  7354  prarloclemarch2  7356  enq0tr  7371  nqnq0  7378  addcmpblnq0  7380  mulcanenq0ec  7382  nnnq0lem1  7383  nqpnq0nq  7390  nq0m0r  7393  nq02m  7402  prarloclemlt  7430  prarloclemcalc  7439  addlocpr  7473  nqprl  7488  nqpru  7489  addnqprlemrl  7494  addnqprlemru  7495  prmuloclemcalc  7502  mullocprlem  7507  mulnqprlemrl  7510  mulnqprlemru  7511  1idprl  7527  1idpru  7528  ltaddpr  7534  ltexprlemm  7537  ltexprlemopl  7538  ltexprlemopu  7540  ltexprlemdisj  7543  ltexprlemrl  7547  ltexprlemru  7549  addcanprleml  7551  addcanprlemu  7552  addcanprg  7553  prplnqu  7557  recexprlemloc  7568  recexprlem1ssl  7570  recexprlem1ssu  7571  aptiprleml  7576  aptiprlemu  7577  archpr  7580  cauappcvgprlemm  7582  cauappcvgprlemopl  7583  cauappcvgprlemloc  7589  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  cauappcvgprlem1  7596  cauappcvgprlem2  7597  caucvgprlemnkj  7603  caucvgprlemopl  7606  caucvgprlemloc  7612  caucvgprlemladdfu  7614  caucvgprlem2  7617  caucvgprprlemnkltj  7626  caucvgprprlemopl  7634  caucvgprprlemloc  7640  caucvgprprlemexbt  7643  caucvgprprlemaddq  7645  caucvgprprlem2  7647  suplocexprlemmu  7655  suplocexprlemru  7656  suplocexprlemloc  7658  suplocexprlemlub  7661  prsrlem1  7679  0idsr  7704  1idsr  7705  recexgt0sr  7710  archsr  7719  prsradd  7723  caucvgsrlemcau  7730  caucvgsrlembound  7731  caucvgsrlemoffgt1  7736  suplocsrlemb  7743  suplocsrlempr  7744  suplocsrlem  7745  pitonnlem1p1  7783  pitonn  7785  pitoregt0  7786  peano2nnnn  7790  recidpirq  7795  axcaucvglemval  7834  leid  7978  nltled  8015  readdcan  8034  addneintrd  8082  addneintr2d  8083  pncan  8100  subsub2  8122  subsub4  8127  negned  8202  subne0d  8214  subneintrd  8249  subneintr2d  8251  subeq0bd  8273  subdi  8279  gt0add  8467  rimul  8479  rereim  8480  ltmul1a  8485  apreim  8497  apirr  8499  mulap0r  8509  msqge0  8510  mulge0  8513  gt0ap0  8520  ltap  8527  subap0d  8538  recexaplem2  8545  mulap0bad  8552  mulap0bbd  8553  mul0eqap  8563  divrecap  8580  div0ap  8594  div1  8595  recrecap  8601  divdivdivap  8605  ddcanap  8618  rerecclap  8622  div2negap  8627  diveqap1bd  8728  recgt0  8741  prodgt0  8743  lemul1a  8749  recp1lt1  8790  squeeze0  8795  peano2nn  8865  div4p1lem1div2  9106  arch  9107  peano2z  9223  peano2zm  9225  ztri3or  9230  nn0n0n1ge2  9257  zextle  9278  gtndiv  9282  suprzclex  9285  nn0ind-raph  9304  uzid  9476  uzneg  9480  uztric  9483  uz11  9484  eluzp1l  9486  qdivcl  9577  irrmul  9581  rpnegap  9618  negelrpd  9620  ledivge1le  9658  mul2lt0rlt0  9691  mul2lt0rgt0  9692  nn0ledivnn  9699  ltpnf  9712  mnflt  9715  pnfge  9721  mnfle  9724  xrlttr  9727  xrltso  9728  xrlttri3  9729  xrleid  9732  xaddass2  9802  xltadd1  9808  xlt2add  9812  xleaddadd  9819  iccf1o  9936  fztri3or  9970  fznlem  9972  fzn  9973  fzsplit2  9981  fznatpl1  10007  uzsplit  10023  fseq1p1m1  10025  fzm1  10031  fznn0sub2  10059  difelfznle  10066  1fv  10070  fzodcel  10083  fzospliti  10107  fzouzsplit  10110  eluzgtdifelfzo  10128  exfzdc  10171  subfzo0  10173  exbtwnz  10182  qbtwnrelemcalc  10187  flqlelt  10207  qfraclt1  10211  qfracge0  10212  flqltnz  10218  btwnzge0  10231  flhalf  10233  ceiqle  10244  intfracq  10251  mulqmod0  10261  modqge0  10263  modqlt  10264  modqid  10280  modqid0  10281  m1modge3gt1  10302  modqltm1p1mod  10307  q2txmodxeq0  10315  modaddmodlo  10319  modsumfzodifsn  10327  addmodlteq  10329  frecuzrdgtcl  10343  frecuzrdgtclt  10352  uzennn  10367  uzsinds  10373  seqf  10392  seqf2  10395  monoord2  10408  iseqf1olemqk  10425  iseqf1olemjpcl  10426  iseqf1olemqpcl  10427  seq3f1olemqsumkj  10429  seq3f1olemqsum  10431  seq3f1olemstep  10432  seq3f1oleml  10434  ser3le  10449  exp3vallem  10452  exp3val  10453  expp1  10458  expcllem  10462  ltexp2a  10503  leexp2a  10504  nn0ltexp2  10619  faclbnd  10650  faclbnd2  10651  faclbnd3  10652  bcval5  10672  bcpasc  10675  hashennn  10689  fihasheqf1oi  10697  hashsng  10707  fihashfn  10709  hashun  10714  fihashss  10725  fihashssdif  10727  hashfz  10730  hashxp  10735  fimaxq  10736  zfz1isolem1  10749  seq3coll  10751  shftfn  10762  cjth  10784  cjmulrcl  10825  reim0bd  10882  rerebd  10883  cjrebd  10884  caucvgre  10919  cvg1nlemcxze  10920  cvg1nlemcau  10922  cvg1nlemres  10923  recvguniq  10933  resqrexlemover  10948  resqrexlemdec  10949  resqrexlemgt0  10958  resqrexlemoverl  10959  resqrexlemglsq  10960  rersqrtthlem  10968  sqrtgt0  10972  leabs  11012  absexpzap  11018  absle  11027  recvalap  11035  abstri  11042  abs2dif  11044  amgm2  11056  absne0d  11125  maxleim  11143  maxabslemab  11144  maxabslemlub  11145  maxltsup  11156  zmaxcl  11162  fimaxre2  11164  minmax  11167  rpmincl  11175  bdtrilem  11176  bdtri  11177  xrmaxleim  11181  xrmaxiflemcom  11186  xrmaxltsup  11195  xrmaxadd  11198  xrminmax  11202  xrminrpcl  11211  climconst  11227  climuni  11230  2clim  11238  climcn1  11245  climcn2  11246  reccn2ap  11250  climge0  11262  climle  11271  climsqz  11272  climsqz2  11273  serf0  11289  summodclem3  11317  summodclem2a  11318  fsumcl2lem  11335  sumpr  11350  sumtp  11351  fsum0diaglem  11377  mptfzshft  11379  fsumle  11400  fsumlt  11401  divcnv  11434  trireciplem  11437  expcnvap0  11439  expcnv  11441  explecnv  11442  geosergap  11443  cvgratnnlembern  11460  cvgratnnlemabsle  11464  cvgratnnlemsumlt  11465  cvgratz  11469  cvgratgt0  11470  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  clim2divap  11477  prodmodclem3  11512  prodmodclem2a  11513  fprodseq  11520  fprodmul  11528  fprodfac  11552  fprodconst  11557  fprodap0  11558  fprodap0f  11573  fprodle  11577  eftcl  11591  ef0lem  11597  efsub  11618  eftlub  11627  eflegeo  11638  tanval2ap  11650  sinadd  11673  cos2t  11687  cos2tsin  11688  sin01bnd  11694  cos01bnd  11695  eirraplem  11713  dvdsval2  11726  dvdsdc  11734  dvds0lem  11737  zdvdsdc  11748  dvdscmulr  11756  dvdsmulcr  11757  dvdslelemd  11777  divconjdvds  11783  dvdsext  11789  fzm1ndvds  11790  dvdsmod  11796  oexpneg  11810  2tp1odd  11817  mulsucdiv2z  11818  2teven  11820  zeo5  11821  opeo  11830  omeo  11831  nn0ob  11841  divalglemnqt  11853  zsupcllemstep  11874  zsupcl  11876  zssinfcl  11877  infssuzex  11878  infssuzcldc  11880  suprzubdc  11881  nninfdcex  11882  gcddvds  11892  dvdslegcd  11893  gcdneg  11911  bezoutlemnewy  11925  bezoutlemstep  11926  bezoutlema  11928  bezoutlemb  11929  bezoutlemmo  11935  bezoutlemle  11937  bezoutlemsup  11938  dfgcd3  11939  bezout  11940  dfgcd2  11943  uzwodc  11966  lcmcllem  11995  lcmneg  12002  lcmgcdlem  12005  lcmdvds  12007  lcmid  12008  3lcm2e6woprm  12014  6lcm4e12  12015  ncoprmgcdne1b  12017  mulgcddvds  12022  divgcdcoprmex  12030  cncongr1  12031  cncongr2  12032  isprm2lem  12044  prmind2  12048  dvdsnprmd  12053  prm2orodd  12054  sqnprm  12064  isprm5lem  12069  rpexp  12081  sqrt2irrlem  12089  oddpwdclemdc  12101  sqrt2irraplemnn  12107  qnumdencoprm  12121  qeqnumdivden  12122  nn0gcdsq  12128  nn0sqrtelqelz  12134  nonsq  12135  phicl2  12142  phibnd  12145  hashdvds  12149  phiprmpw  12150  phimullem  12153  eulerthlemrprm  12157  eulerthlema  12158  eulerthlemth  12160  prmdiveq  12164  hashgcdlem  12166  odzdvds  12173  modprminv  12177  nnnn0modprm0  12183  modprmn0modprm0  12184  pythagtriplem10  12197  pythagtriplem19  12210  pythagtrip  12211  pcpre1  12220  pcpremul  12221  pceu  12223  pcmul  12229  pcdiv  12230  pcqmul  12231  pcqdiv  12235  pcexp  12237  pcdvdsb  12247  pcidlem  12250  pcdvdstr  12254  pcgcd1  12255  pc2dvds  12257  pcprmpw2  12260  difsqpwdvds  12265  pcaddlem  12266  pcadd  12267  pcmpt  12269  pcmptdvds  12271  pcprod  12272  fldivp1  12274  pcfaclem  12275  pcfac  12276  pcbc  12277  qexpz  12278  pockthlem  12282  pockthg  12283  1arithlem4  12292  1arith  12293  1arith2  12294  4sqlem6  12309  4sqlem8  12311  4sqlem9  12312  4sqlem10  12313  znnen  12327  ennnfonelemk  12329  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ennnfonelemrnh  12345  ennnfonelemfun  12346  ennnfonelemf1  12347  ennnfonelemrn  12348  ennnfonelemnn0  12351  ctinfomlemom  12356  ctiunctlemudc  12366  unct  12371  omctfn  12372  ssnnctlemct  12375  nninfdclemp1  12379  nninfdc  12382  structfung  12407  setsfun  12425  setsfun0  12426  setscom  12430  setsslid  12440  baspartn  12648  eltg3i  12656  tgclb  12665  topbas  12667  2basgeng  12682  topcld  12709  0cld  12712  uncld  12713  neif  12741  elnei  12752  0nei  12766  restbasg  12768  iscnp4  12818  cnpnei  12819  cnclima  12823  cncnp  12830  cnrest2r  12837  cndis  12841  lmff  12849  lmtopcnp  12850  txbas  12858  txopn  12865  txcnp  12871  upxp  12872  txdis1cn  12878  cnmpt11  12883  cnmpt21  12891  psmetge0  12931  xmetge0  12965  xmettpos  12970  xmetrtri  12976  metrtri  12977  xblpnfps  12998  xblpnf  12999  blfps  13009  blf  13010  ssblps  13025  ssbl  13026  blbas  13033  metss2  13098  xmettxlem  13109  xmettx  13110  qtopbas  13122  divcnap  13155  cncfss  13170  cdivcncfap  13187  expcncf  13192  cnopnap  13194  dedekindeulemuub  13195  dedekindeulemlu  13199  dedekindeu  13201  suplociccex  13203  dedekindicclemuub  13204  dedekindicclemlu  13208  dedekindicclemicc  13210  ivthinclemlopn  13214  ivthinclemuopn  13216  ivthinc  13221  ellimc3apf  13229  limcimolemlt  13233  limcimo  13234  limcresi  13235  cnplimclemle  13237  reldvg  13248  dvfgg  13257  dvidlemap  13260  dvcjbr  13272  dvcj  13273  dvrecap  13277  dveflem  13287  dvef  13288  reeff1oleme  13293  pilem3  13304  sinq34lt0t  13352  cosq14gt0  13353  coseq0q4123  13355  tangtx  13359  sincosq1eq  13360  cosordlem  13370  logdivlti  13402  relogbval  13469  relogbzcl  13470  nnlogbexp  13477  logbgcd1irr  13485  logbgcd1irraplemexp  13486  logbgcd1irraplemap  13487  zabsle1  13500  lgslem1  13501  lgsval  13505  lgsfvalg  13506  lgsfcl2  13507  lgsval2lem  13511  lgscl1  13524  lgsmod  13527  lgsdir2lem5  13533  lgsdir2  13534  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  2sqlem3  13553  2sqlem8  13559  2sqlem10  13561  fnmptd  13646  bj-sels  13756  bj-nnelon  13801  pwle2  13838  pwf1oexmid  13839  pw1nct  13843  nninfall  13849  nninfsellemdc  13850  nninfself  13853  refeq  13867  isomninnlem  13869  cvgcmp2nlemabs  13871  trilpolemlt1  13880  trirec0  13883  apdifflemf  13885  apdifflemr  13886  apdiff  13887  iswomninnlem  13888  iswomni0  13890  ismkvnnlem  13891  reap0  13897