Theorem mpbird 167

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 158	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝜓)

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  2273  eqnetrd  2391  3netr4d  2400  r19.30dc  2644  raleqtrrdv  2703  rexeqtrrdv  2704  sbcne12g  3102  eqsstrd  3220  3sstr4d  3229  eqbrtrd  4056  3brtr4d  4066  snelpwi  4246  prelpwi  4248  pwel  4252  ordelon  4419  onin  4422  elelsuc  4445  onsuc  4538  onsucb  4540  onintonm  4554  omsinds  4659  sosng  4737  relssdv  4756  eqbrrdv  4761  eqrelrdv2  4763  relsnopg  4768  breldmg  4873  elrnmptdv  4921  iss  4993  xpimasn  5119  elxp4  5158  elxp5  5159  iotam  5251  funssres  5301  f0rn0  5455  fimadmfo  5492  sefvex  5582  fvun1  5630  eqfnfvd  5665  fvimacnvi  5679  fvimacnv  5680  fvelrn  5696  fmpt3d  5721  fmpt2d  5727  resflem  5729  fmptco  5731  fsn  5737  ftpg  5749  fconst2g  5780  funfvima3  5799  elabrexg  5808  foeqcnvco  5840  f1eqcocnv  5841  fliftfun  5846  fliftfund  5847  fliftval  5850  riota5f  5905  f1ofveu  5913  f1ocnvd  6129  f1opw2  6133  off  6152  offval2  6155  ofrfval2  6156  offveq  6160  caofref  6164  caofinvl  6165  elxp6  6236  cnvf1olem  6291  f2ndf  6293  f1od2  6302  tposf12  6336  smores2  6361  tfrlemisucaccv  6392  tfrlemibfn  6395  tfr1onlemsucaccv  6408  tfr1onlembfn  6411  tfrcllemsucaccv  6421  tfrcllembfn  6424  tfrcl  6431  tfri3  6434  frecabcl  6466  nnsucsssuc  6559  ersym  6613  ertr  6616  swoer  6629  erth  6647  riinerm  6676  qliftfund  6686  eroprf  6696  ecopoverg  6704  th3qlem1  6705  elmapssres  6741  mapss  6759  fdiagfn  6760  ixpssmap2g  6795  mapsnf1o  6805  f1dom2g  6824  dom3d  6842  pw2f1odclem  6904  fopwdom  6906  mapxpen  6918  nndomo  6934  dif1en  6949  findcard2  6959  findcard2s  6960  diffisn  6963  fimax2gtrilemstep  6970  fientri3  6985  tpfidceq  7000  fiintim  7001  opabfi  7008  f1dmvrnfibi  7019  sbthlemi6  7037  elfir  7048  fifo  7055  supelti  7077  supsnti  7080  cnvinfex  7093  ordiso2  7110  updjud  7157  djudom  7168  difinfsn  7175  ctssdc  7188  enumctlemm  7189  enumct  7190  nninfninc  7198  enomnilem  7213  fodjuf  7220  ismkvnex  7230  omnimkv  7231  enmkvlem  7236  enwomnilem  7244  nninfdcinf  7246  nninfwlporlem  7248  isnumi  7262  exmidfodomrlemrALT  7284  finacn  7289  djudoml  7304  djudomr  7305  netap  7339  2omotaplemap  7342  2omotaplemst  7343  exmidapne  7345  cc2lem  7351  cc3  7353  ltsopi  7406  pitri3or  7408  ltdcpi  7409  indpi  7428  enqdc  7447  enqdc1  7448  addcmpblnq  7453  mulcanenq  7471  recrecnq  7480  nqtri3or  7482  ltdcnq  7483  ltsonq  7484  ltaddnq  7493  subhalfnqq  7500  archnqq  7503  prarloclemarch2  7505  enq0tr  7520  nqnq0  7527  addcmpblnq0  7529  mulcanenq0ec  7531  nnnq0lem1  7532  nqpnq0nq  7539  nq0m0r  7542  nq02m  7551  prarloclemlt  7579  prarloclemcalc  7588  addlocpr  7622  nqprl  7637  nqpru  7638  addnqprlemrl  7643  addnqprlemru  7644  prmuloclemcalc  7651  mullocprlem  7656  mulnqprlemrl  7659  mulnqprlemru  7660  1idprl  7676  1idpru  7677  ltaddpr  7683  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemopu  7689  ltexprlemdisj  7692  ltexprlemrl  7696  ltexprlemru  7698  addcanprleml  7700  addcanprlemu  7701  addcanprg  7702  prplnqu  7706  recexprlemloc  7717  recexprlem1ssl  7719  recexprlem1ssu  7720  aptiprleml  7725  aptiprlemu  7726  archpr  7729  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemloc  7738  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlem1  7745  cauappcvgprlem2  7746  caucvgprlemnkj  7752  caucvgprlemopl  7755  caucvgprlemloc  7761  caucvgprlemladdfu  7763  caucvgprlem2  7766  caucvgprprlemnkltj  7775  caucvgprprlemopl  7783  caucvgprprlemloc  7789  caucvgprprlemexbt  7792  caucvgprprlemaddq  7794  caucvgprprlem2  7796  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemloc  7807  suplocexprlemlub  7810  prsrlem1  7828  0idsr  7853  1idsr  7854  recexgt0sr  7859  archsr  7868  prsradd  7872  caucvgsrlemcau  7879  caucvgsrlembound  7880  caucvgsrlemoffgt1  7885  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  pitonnlem1p1  7932  pitonn  7934  pitoregt0  7935  peano2nnnn  7939  recidpirq  7944  axcaucvglemval  7983  leid  8129  nltled  8166  readdcan  8185  addneintrd  8233  addneintr2d  8234  pncan  8251  subsub2  8273  subsub4  8278  negned  8353  subne0d  8365  subneintrd  8400  subneintr2d  8402  subeq0bd  8424  subdi  8430  gt0add  8619  rimul  8631  rereim  8632  ltmul1a  8637  apreim  8649  apirr  8651  mulap0r  8661  msqge0  8662  mulge0  8665  gt0ap0  8672  ltap  8679  subap0d  8690  recexaplem2  8698  mulap0bad  8705  mulap0bbd  8706  mul0eqap  8716  divrecap  8734  div0ap  8748  div1  8749  recrecap  8755  divdivdivap  8759  ddcanap  8772  rerecclap  8776  div2negap  8781  diveqap1bd  8882  recgt0  8896  prodgt0  8898  lemul1a  8904  recp1lt1  8945  squeeze0  8950  peano2nn  9021  div4p1lem1div2  9264  arch  9265  peano2z  9381  peano2zm  9383  ztri3or  9388  nn0n0n1ge2  9415  zextle  9436  gtndiv  9440  suprzclex  9443  nn0ind-raph  9462  uzid  9634  uzneg  9639  uztric  9642  uz11  9643  eluzp1l  9645  qdivcl  9736  irrmul  9740  irrmulap  9741  rpnegap  9780  negelrpd  9782  ledivge1le  9820  mul2lt0rlt0  9853  mul2lt0rgt0  9854  nn0ledivnn  9861  ltpnf  9874  mnflt  9877  pnfge  9883  mnfle  9886  xrlttr  9889  xrltso  9890  xrlttri3  9891  xrleid  9894  xaddass2  9964  xltadd1  9970  xlt2add  9974  xleaddadd  9981  iccf1o  10098  fztri3or  10133  fznlem  10135  fzn  10136  fzsplit2  10144  fznatpl1  10170  uzsplit  10186  fseq1p1m1  10188  fzm1  10194  fznn0sub2  10222  difelfznle  10229  1fv  10233  fzodcel  10247  fzospliti  10271  fzouzsplit  10274  eluzgtdifelfzo  10292  exfzdc  10335  subfzo0  10337  zsupcllemstep  10338  zsupcl  10340  zssinfcl  10341  infssuzex  10342  infssuzcldc  10344  suprzubdc  10345  nninfdcex  10346  qdcle  10355  exbtwnz  10359  qbtwnrelemcalc  10364  flqlelt  10385  qfraclt1  10389  qfracge0  10390  flqltnz  10396  btwnzge0  10409  flhalf  10411  fldiv4lem1div2uz2  10415  ceiqle  10424  intfracq  10431  mulqmod0  10441  modqge0  10443  modqlt  10444  modqid  10460  modqid0  10461  m1modge3gt1  10482  modqltm1p1mod  10487  q2txmodxeq0  10495  modaddmodlo  10499  modsumfzodifsn  10507  addmodlteq  10509  frecuzrdgtcl  10523  frecuzrdgtclt  10532  uzennn  10547  uzsinds  10555  seqf  10575  seqf2  10579  monoord2  10597  iseqf1olemqk  10618  iseqf1olemjpcl  10619  iseqf1olemqpcl  10620  seq3f1olemqsumkj  10622  seq3f1olemqsum  10624  seq3f1olemstep  10625  seq3f1oleml  10627  seqf1oglem1  10630  ser3le  10648  exp3vallem  10651  exp3val  10652  expp1  10657  expcllem  10661  ltexp2a  10702  leexp2a  10703  nn0ltexp2  10820  faclbnd  10852  faclbnd2  10853  faclbnd3  10854  bcval5  10874  bcpasc  10877  hashennn  10891  fihasheqf1oi  10898  hashsng  10909  fihashfn  10911  hashun  10916  fihashss  10927  fihashssdif  10929  hashfz  10932  hashxp  10937  fimaxq  10938  zfz1isolem1  10951  seq3coll  10953  wrdf  10960  wrdlenge2n0  10989  fstwrdne0  10993  wrdred1hash  10997  shftfn  11008  cjth  11030  cjmulrcl  11071  reim0bd  11128  rerebd  11129  cjrebd  11130  caucvgre  11165  cvg1nlemcxze  11166  cvg1nlemcau  11168  cvg1nlemres  11169  recvguniq  11179  resqrexlemover  11194  resqrexlemdec  11195  resqrexlemgt0  11204  resqrexlemoverl  11205  resqrexlemglsq  11206  rersqrtthlem  11214  sqrtgt0  11218  leabs  11258  absexpzap  11264  absle  11273  recvalap  11281  abstri  11288  abs2dif  11290  amgm2  11302  absne0d  11371  maxleim  11389  maxabslemab  11390  maxabslemlub  11391  maxltsup  11402  zmaxcl  11408  fimaxre2  11411  minmax  11414  rpmincl  11422  bdtrilem  11423  bdtri  11424  xrmaxleim  11428  xrmaxiflemcom  11433  xrmaxltsup  11442  xrmaxadd  11445  xrminmax  11449  xrminrpcl  11458  climconst  11474  climuni  11477  2clim  11485  climcn1  11492  climcn2  11493  reccn2ap  11497  climge0  11509  climle  11518  climsqz  11519  climsqz2  11520  serf0  11536  summodclem3  11564  summodclem2a  11565  fsumcl2lem  11582  sumpr  11597  sumtp  11598  fsum0diaglem  11624  mptfzshft  11626  fsumle  11647  fsumlt  11648  divcnv  11681  trireciplem  11684  expcnvap0  11686  expcnv  11688  explecnv  11689  geosergap  11690  cvgratnnlembern  11707  cvgratnnlemabsle  11711  cvgratnnlemsumlt  11712  cvgratz  11716  cvgratgt0  11717  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  clim2divap  11724  prodmodclem3  11759  prodmodclem2a  11760  fprodseq  11767  fprodmul  11775  fprodfac  11799  fprodconst  11804  fprodap0  11805  fprodap0f  11820  fprodle  11824  eftcl  11838  ef0lem  11844  efsub  11865  eftlub  11874  eflegeo  11885  tanval2ap  11897  sinadd  11920  cos2t  11934  cos2tsin  11935  sin01bnd  11941  cos01bnd  11942  eirraplem  11961  dvdsval2  11974  dvdsdc  11982  dvds0lem  11985  zdvdsdc  11996  dvdscmulr  12004  dvdsmulcr  12005  fsumdvds  12026  dvdslelemd  12027  divconjdvds  12033  dvdsext  12039  fzm1ndvds  12040  dvdsmod  12046  3dvds  12048  oexpneg  12061  2tp1odd  12068  mulsucdiv2z  12069  2teven  12071  zeo5  12072  opeo  12081  omeo  12082  nn0ob  12092  divalglemnqt  12104  bitsdc  12131  bits0o  12134  bitsfzolem  12138  bitsfzo  12139  bitsmod  12140  bitscmp  12142  bitsinv1lem  12145  gcddvds  12157  dvdslegcd  12158  gcdneg  12176  bezoutlemnewy  12190  bezoutlemstep  12191  bezoutlema  12193  bezoutlemb  12194  bezoutlemmo  12200  bezoutlemle  12202  bezoutlemsup  12203  dfgcd3  12204  bezout  12205  dfgcd2  12208  uzwodc  12231  lcmcllem  12262  lcmneg  12269  lcmgcdlem  12272  lcmdvds  12274  lcmid  12275  3lcm2e6woprm  12281  6lcm4e12  12282  ncoprmgcdne1b  12284  mulgcddvds  12289  divgcdcoprmex  12297  cncongr1  12298  cncongr2  12299  isprm2lem  12311  prmind2  12315  dvdsnprmd  12320  prm2orodd  12321  sqnprm  12331  isprm5lem  12336  rpexp  12348  sqrt2irrlem  12356  oddpwdclemdc  12368  sqrt2irraplemnn  12374  qnumdencoprm  12388  qeqnumdivden  12389  nn0gcdsq  12395  nn0sqrtelqelz  12401  nonsq  12402  phicl2  12409  phibnd  12412  hashdvds  12416  phiprmpw  12417  phimullem  12420  eulerthlemrprm  12424  eulerthlema  12425  eulerthlemth  12427  prmdiveq  12431  hashgcdlem  12433  odzdvds  12441  modprminv  12445  nnnn0modprm0  12451  modprmn0modprm0  12452  pythagtriplem10  12465  pythagtriplem19  12478  pythagtrip  12479  pcpre1  12488  pcpremul  12489  pceu  12491  pcmul  12497  pcdiv  12498  pcqmul  12499  pcqdiv  12503  pcexp  12505  pcdvdsb  12516  pcidlem  12519  pcdvdstr  12523  pcgcd1  12524  pc2dvds  12526  pcprmpw2  12529  difsqpwdvds  12534  pcaddlem  12535  pcadd  12536  pcadd2  12537  pcmpt  12539  pcmptdvds  12541  pcprod  12542  fldivp1  12544  pcfaclem  12545  pcfac  12546  pcbc  12547  qexpz  12548  pockthlem  12552  pockthg  12553  1arithlem4  12562  1arith  12563  1arith2  12564  4sqlem6  12579  4sqlem8  12581  4sqlem9  12582  4sqlem10  12583  4sqexercise1  12594  4sqexercise2  12595  4sqlemsdc  12596  4sqlem11  12597  4sqlem12  12598  4sqlem15  12601  4sqlem16  12602  4sqlem17  12603  znnen  12642  ennnfonelemk  12644  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemrnh  12660  ennnfonelemfun  12661  ennnfonelemf1  12662  ennnfonelemrn  12663  ennnfonelemnn0  12666  ctinfomlemom  12671  ctiunctlemudc  12681  unct  12686  omctfn  12687  ssnnctlemct  12690  nninfdclemp1  12694  nninfdc  12697  structfung  12722  setsfun  12740  setsfun0  12741  setscom  12745  strslfv3  12751  setsslid  12756  pwsdiagel  13001  pwssnf1o  13002  imasaddfnlemg  13018  imasaddvallemg  13019  mgmsscl  13065  plusffng  13069  mgmplusf  13070  mgm0  13073  mgm1  13074  opifismgmdc  13075  gsumfzval  13095  gsumprval  13103  sgrp1  13115  issgrpd  13116  prdsplusgsgrpcl  13118  mndpfo  13142  mndfo  13143  prdsplusgcl  13150  prdsidlem  13151  mnd1  13159  0subm  13188  mhmima  13195  grpinvfng  13248  isgrpinv  13258  grpinvid  13264  grpinvf1o  13274  grpinvadd  13282  grpsubf  13283  grpsubsub4  13297  grplactcnv  13306  grp1  13310  grp1inv  13311  prdsinvlem  13312  prdsinvgd  13314  qusgrp2  13321  mulgfng  13332  subginv  13389  resgrpisgrp  13403  subgintm  13406  0subg  13407  0nsg  13422  qusinv  13444  ghminv  13458  ghmrn  13465  ghmeql  13475  ghmnsgima  13476  kerf1ghm  13482  conjnmz  13487  rngass  13573  rngmneg1  13581  rngmneg2  13582  qusrng  13592  srgideu  13606  srgidmlem  13612  srgpcomp  13624  srg1expzeq1  13629  ringcl  13647  ringideu  13651  ringidmlem  13656  ringnegl  13685  ringnegr  13686  ring1  13693  qusring2  13700  opprringbg  13714  dvdsrd  13728  dvdsr01  13738  isunitd  13740  unitinvcl  13757  unitinvinv  13758  unitnegcl  13764  rhmmul  13798  rhmf1o  13802  nzrunit  13822  lringuplu  13830  subrngintm  13846  subrgsubm  13868  subrgintm  13877  aprsym  13918  scaffng  13943  lmodscaf  13944  lsssn0  14004  lss1d  14017  lssintclm  14018  lspval  14024  lspcl  14025  lspsnid  14041  lspprid1  14045  lspsn  14050  sraval  14071  rspcl  14125  rspssid  14126  rspssp  14128  rnglidlmmgm  14130  rnglidlmsgrp  14131  cnfldneg  14207  zringinvg  14238  expghmap  14241  znzrhfo  14282  znf1o  14285  znhash  14290  znidomb  14292  znrrg  14294  psraddcl  14310  psr0cl  14311  psrnegcl  14313  psrneg  14317  psr1clfi  14318  baspartn  14372  eltg3i  14378  tgclb  14387  topbas  14389  2basgeng  14404  topcld  14431  0cld  14434  uncld  14435  neif  14463  elnei  14474  0nei  14488  restbasg  14490  iscnp4  14540  cnpnei  14541  cnclima  14545  cncnp  14552  cnrest2r  14559  cndis  14563  lmff  14571  lmtopcnp  14572  txbas  14580  txopn  14587  txcnp  14593  upxp  14594  txdis1cn  14600  cnmpt11  14605  cnmpt21  14613  psmetge0  14653  xmetge0  14687  xmettpos  14692  xmetrtri  14698  metrtri  14699  xblpnfps  14720  xblpnf  14721  blfps  14731  blf  14732  ssblps  14747  ssbl  14748  blbas  14755  metss2  14820  xmettxlem  14831  xmettx  14832  qtopbas  14844  divcnap  14887  cncfss  14905  cdivcncfap  14926  expcncf  14931  cnopnap  14933  maxcncf  14937  mincncf  14938  dedekindeulemuub  14939  dedekindeulemlu  14943  dedekindeu  14945  suplociccex  14947  dedekindicclemuub  14948  dedekindicclemlu  14952  dedekindicclemicc  14954  ivthinclemlopn  14958  ivthinclemuopn  14960  ivthinc  14965  ivthreinc  14967  hoverlt1  14971  ellimc3apf  14982  limcimolemlt  14986  limcimo  14987  limcresi  14988  cnplimclemle  14990  reldvg  15001  dvfgg  15010  dvidlemap  15013  dvidrelem  15014  dvidsslem  15015  dvcjbr  15030  dvcj  15031  dvrecap  15035  dveflem  15048  dvef  15049  elply2  15057  elplyr  15062  plycj  15083  plyreres  15086  reeff1oleme  15094  pilem3  15105  sinq34lt0t  15153  cosq14gt0  15154  coseq0q4123  15156  tangtx  15160  sincosq1eq  15161  cosordlem  15171  logdivlti  15203  relogbval  15273  relogbzcl  15274  nnlogbexp  15281  logbgcd1irr  15289  logbgcd1irraplemexp  15290  logbgcd1irraplemap  15291  wilthlem1  15302  mpodvdsmulf1o  15312  mersenne  15319  perfectlem2  15322  perfect  15323  zabsle1  15326  lgslem1  15327  lgsval  15331  lgsfvalg  15332  lgsfcl2  15333  lgsval2lem  15337  lgscl1  15350  lgsmod  15353  lgsdir2lem5  15359  lgsdir2  15360  lgsdilem2  15363  lgsdi  15364  lgsne0  15365  gausslemma2dlem0c  15378  gausslemma2dlem0h  15383  gausslemma2dlem1a  15385  gausslemma2dlem1f1o  15387  gausslemma2dlem3  15390  lgseisenlem1  15397  lgseisenlem2  15398  lgseisenlem3  15399  lgseisenlem4  15400  lgseisen  15401  lgsquadlem1  15404  lgsquadlem2  15405  lgsquadlem3  15406  lgsquad3  15411  2lgslem3b1  15425  2lgslem3c1  15426  2lgs  15431  2lgsoddprmlem2  15433  2lgsoddprm  15440  2sqlem3  15444  2sqlem8  15450  2sqlem10  15452  fnmptd  15536  bj-sels  15646  bj-nnelon  15691  2omap  15728  pwle2  15731  pwf1oexmid  15732  pw1nct  15736  nninfall  15742  nninfsellemdc  15743  nninfself  15746  nnnninfex  15755  nninfnfiinf  15756  refeq  15763  isomninnlem  15765  cvgcmp2nlemabs  15767  trilpolemlt1  15776  trirec0  15779  apdifflemf  15781  apdifflemr  15782  apdiff  15783  iswomninnlem  15784  iswomni0  15786  ismkvnnlem  15787  reap0  15793  cndcap  15794