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  708  pm4.55dc  941  mpbir2and  947  pm3.12dc  961  mpbir3and  1183  pm5.15dc  1409  eqeltrd  2283  eqnetrd  2401  3netr4d  2410  r19.30dc  2654  raleqtrrdv  2713  rexeqtrrdv  2714  sbcne12g  3112  eqsstrd  3230  3sstr4d  3239  eqbrtrd  4069  3brtr4d  4079  snelpwi  4260  prelpwi  4262  pwel  4266  ordelon  4434  onin  4437  elelsuc  4460  onsuc  4553  onsucb  4555  onintonm  4569  omsinds  4674  sosng  4752  relssdv  4771  eqbrrdv  4776  eqrelrdv2  4778  relsnopg  4783  breldmg  4889  elrnmptdv  4937  iss  5010  xpimasn  5136  elxp4  5175  elxp5  5176  iotam  5268  funssres  5318  f0rn0  5477  fimadmfo  5514  sefvex  5604  fvun1  5652  eqfnfvd  5687  fvimacnvi  5701  fvimacnv  5702  fvelrn  5718  fmpt3d  5743  fmpt2d  5749  resflem  5751  fmptco  5753  fsn  5759  funopsn  5769  ftpg  5775  fconst2g  5806  funfvima3  5825  elabrexg  5834  foeqcnvco  5866  f1eqcocnv  5867  fliftfun  5872  fliftfund  5873  fliftval  5876  riota5f  5931  f1ofveu  5939  f1ocnvd  6155  f1opw2  6159  off  6178  offval2  6181  ofrfval2  6182  offveq  6186  caofref  6190  caofinvl  6191  elxp6  6262  cnvf1olem  6317  f2ndf  6319  f1od2  6328  tposf12  6362  smores2  6387  tfrlemisucaccv  6418  tfrlemibfn  6421  tfr1onlemsucaccv  6434  tfr1onlembfn  6437  tfrcllemsucaccv  6447  tfrcllembfn  6450  tfrcl  6457  tfri3  6460  frecabcl  6492  nnsucsssuc  6585  ersym  6639  ertr  6642  swoer  6655  erth  6673  riinerm  6702  qliftfund  6712  eroprf  6722  ecopoverg  6730  th3qlem1  6731  elmapssres  6767  mapss  6785  fdiagfn  6786  ixpssmap2g  6821  mapsnf1o  6831  f1oen4g  6850  f1dom4g  6851  f1dom2g  6854  dom3d  6872  en2prd  6916  pw2f1odclem  6938  fopwdom  6940  mapxpen  6952  nndomo  6968  dif1en  6983  findcard2  6993  findcard2s  6994  diffisn  6997  fimax2gtrilemstep  7004  fientri3  7019  tpfidceq  7034  fiintim  7035  opabfi  7042  f1dmvrnfibi  7053  sbthlemi6  7071  elfir  7082  fifo  7089  supelti  7111  supsnti  7114  cnvinfex  7127  ordiso2  7144  updjud  7191  djudom  7202  difinfsn  7209  ctssdc  7222  enumctlemm  7223  enumct  7224  nninfninc  7232  enomnilem  7247  fodjuf  7254  ismkvnex  7264  omnimkv  7265  enmkvlem  7270  enwomnilem  7278  nninfdcinf  7280  nninfwlporlem  7282  isnumi  7296  exmidfodomrlemrALT  7318  finacn  7323  djudoml  7338  djudomr  7339  netap  7373  2omotaplemap  7376  2omotaplemst  7377  exmidapne  7379  cc2lem  7385  cc3  7387  ltsopi  7440  pitri3or  7442  ltdcpi  7443  indpi  7462  enqdc  7481  enqdc1  7482  addcmpblnq  7487  mulcanenq  7505  recrecnq  7514  nqtri3or  7516  ltdcnq  7517  ltsonq  7518  ltaddnq  7527  subhalfnqq  7534  archnqq  7537  prarloclemarch2  7539  enq0tr  7554  nqnq0  7561  addcmpblnq0  7563  mulcanenq0ec  7565  nnnq0lem1  7566  nqpnq0nq  7573  nq0m0r  7576  nq02m  7585  prarloclemlt  7613  prarloclemcalc  7622  addlocpr  7656  nqprl  7671  nqpru  7672  addnqprlemrl  7677  addnqprlemru  7678  prmuloclemcalc  7685  mullocprlem  7690  mulnqprlemrl  7693  mulnqprlemru  7694  1idprl  7710  1idpru  7711  ltaddpr  7717  ltexprlemm  7720  ltexprlemopl  7721  ltexprlemopu  7723  ltexprlemdisj  7726  ltexprlemrl  7730  ltexprlemru  7732  addcanprleml  7734  addcanprlemu  7735  addcanprg  7736  prplnqu  7740  recexprlemloc  7751  recexprlem1ssl  7753  recexprlem1ssu  7754  aptiprleml  7759  aptiprlemu  7760  archpr  7763  cauappcvgprlemm  7765  cauappcvgprlemopl  7766  cauappcvgprlemloc  7772  cauappcvgprlemladdfu  7774  cauappcvgprlemladdfl  7775  cauappcvgprlem1  7779  cauappcvgprlem2  7780  caucvgprlemnkj  7786  caucvgprlemopl  7789  caucvgprlemloc  7795  caucvgprlemladdfu  7797  caucvgprlem2  7800  caucvgprprlemnkltj  7809  caucvgprprlemopl  7817  caucvgprprlemloc  7823  caucvgprprlemexbt  7826  caucvgprprlemaddq  7828  caucvgprprlem2  7830  suplocexprlemmu  7838  suplocexprlemru  7839  suplocexprlemloc  7841  suplocexprlemlub  7844  prsrlem1  7862  0idsr  7887  1idsr  7888  recexgt0sr  7893  archsr  7902  prsradd  7906  caucvgsrlemcau  7913  caucvgsrlembound  7914  caucvgsrlemoffgt1  7919  suplocsrlemb  7926  suplocsrlempr  7927  suplocsrlem  7928  pitonnlem1p1  7966  pitonn  7968  pitoregt0  7969  peano2nnnn  7973  recidpirq  7978  axcaucvglemval  8017  leid  8163  nltled  8200  readdcan  8219  addneintrd  8267  addneintr2d  8268  pncan  8285  subsub2  8307  subsub4  8312  negned  8387  subne0d  8399  subneintrd  8434  subneintr2d  8436  subeq0bd  8458  subdi  8464  gt0add  8653  rimul  8665  rereim  8666  ltmul1a  8671  apreim  8683  apirr  8685  mulap0r  8695  msqge0  8696  mulge0  8699  gt0ap0  8706  ltap  8713  subap0d  8724  recexaplem2  8732  mulap0bad  8739  mulap0bbd  8740  mul0eqap  8750  divrecap  8768  div0ap  8782  div1  8783  recrecap  8789  divdivdivap  8793  ddcanap  8806  rerecclap  8810  div2negap  8815  diveqap1bd  8916  recgt0  8930  prodgt0  8932  lemul1a  8938  recp1lt1  8979  squeeze0  8984  peano2nn  9055  div4p1lem1div2  9298  arch  9299  peano2z  9415  peano2zm  9417  ztri3or  9422  nn0n0n1ge2  9450  zextle  9471  gtndiv  9475  suprzclex  9478  nn0ind-raph  9497  uzid  9669  uzneg  9674  uztric  9677  uz11  9678  eluzp1l  9680  qdivcl  9771  irrmul  9775  irrmulap  9776  rpnegap  9815  negelrpd  9817  ledivge1le  9855  mul2lt0rlt0  9888  mul2lt0rgt0  9889  nn0ledivnn  9896  ltpnf  9909  mnflt  9912  pnfge  9918  mnfle  9921  xrlttr  9924  xrltso  9925  xrlttri3  9926  xrleid  9929  xaddass2  9999  xltadd1  10005  xlt2add  10009  xleaddadd  10016  iccf1o  10133  fztri3or  10168  fznlem  10170  fzn  10171  fzsplit2  10179  fznatpl1  10205  uzsplit  10221  fseq1p1m1  10223  fzm1  10229  fznn0sub2  10257  difelfznle  10264  1fv  10268  fzodcel  10282  fzospliti  10307  fzouzsplit  10310  eluzgtdifelfzo  10333  exfzdc  10376  subfzo0  10378  zsupcllemstep  10379  zsupcl  10381  zssinfcl  10382  infssuzex  10383  infssuzcldc  10385  suprzubdc  10386  nninfdcex  10387  qdcle  10396  exbtwnz  10400  qbtwnrelemcalc  10405  flqlelt  10426  qfraclt1  10430  qfracge0  10431  flqltnz  10437  btwnzge0  10450  flhalf  10452  fldiv4lem1div2uz2  10456  ceiqle  10465  intfracq  10472  mulqmod0  10482  modqge0  10484  modqlt  10485  modqid  10501  modqid0  10502  m1modge3gt1  10523  modqltm1p1mod  10528  q2txmodxeq0  10536  modaddmodlo  10540  modsumfzodifsn  10548  addmodlteq  10550  frecuzrdgtcl  10564  frecuzrdgtclt  10573  uzennn  10588  uzsinds  10596  seqf  10616  seqf2  10620  monoord2  10638  iseqf1olemqk  10659  iseqf1olemjpcl  10660  iseqf1olemqpcl  10661  seq3f1olemqsumkj  10663  seq3f1olemqsum  10665  seq3f1olemstep  10666  seq3f1oleml  10668  seqf1oglem1  10671  ser3le  10689  exp3vallem  10692  exp3val  10693  expp1  10698  expcllem  10702  ltexp2a  10743  leexp2a  10744  nn0ltexp2  10861  faclbnd  10893  faclbnd2  10894  faclbnd3  10895  bcval5  10915  bcpasc  10918  hashennn  10932  fihasheqf1oi  10939  hashsng  10950  fihashfn  10952  hashun  10957  fihashss  10968  fihashssdif  10970  hashfz  10973  hashxp  10978  fimaxq  10979  zfz1isolem1  10992  seq3coll  10994  hashdmprop2dom  10996  wrdf  11007  wrdlenge2n0  11036  fstwrdne0  11040  wrdred1hash  11044  ccatvalfn  11065  ccatsymb  11066  ccatlid  11070  ccatrid  11071  ccatrn  11073  eqs1  11090  ccats1val2  11100  fzowrddc  11108  swrdlen  11113  swrdnd  11120  swrd0g  11121  swrdfv2  11124  swrdwrdsymbg  11125  pfxn0  11147  pfxwrdsymbg  11149  pfxsuff1eqwrdeq  11158  swrdswrd  11164  shftfn  11179  cjth  11201  cjmulrcl  11242  reim0bd  11299  rerebd  11300  cjrebd  11301  caucvgre  11336  cvg1nlemcxze  11337  cvg1nlemcau  11339  cvg1nlemres  11340  recvguniq  11350  resqrexlemover  11365  resqrexlemdec  11366  resqrexlemgt0  11375  resqrexlemoverl  11376  resqrexlemglsq  11377  rersqrtthlem  11385  sqrtgt0  11389  leabs  11429  absexpzap  11435  absle  11444  recvalap  11452  abstri  11459  abs2dif  11461  amgm2  11473  absne0d  11542  maxleim  11560  maxabslemab  11561  maxabslemlub  11562  maxltsup  11573  zmaxcl  11579  fimaxre2  11582  minmax  11585  rpmincl  11593  bdtrilem  11594  bdtri  11595  xrmaxleim  11599  xrmaxiflemcom  11604  xrmaxltsup  11613  xrmaxadd  11616  xrminmax  11620  xrminrpcl  11629  climconst  11645  climuni  11648  2clim  11656  climcn1  11663  climcn2  11664  reccn2ap  11668  climge0  11680  climle  11689  climsqz  11690  climsqz2  11691  serf0  11707  summodclem3  11735  summodclem2a  11736  fsumcl2lem  11753  sumpr  11768  sumtp  11769  fsum0diaglem  11795  mptfzshft  11797  fsumle  11818  fsumlt  11819  divcnv  11852  trireciplem  11855  expcnvap0  11857  expcnv  11859  explecnv  11860  geosergap  11861  cvgratnnlembern  11878  cvgratnnlemabsle  11882  cvgratnnlemsumlt  11883  cvgratz  11887  cvgratgt0  11888  mertenslemi1  11890  mertenslem2  11891  mertensabs  11892  clim2divap  11895  prodmodclem3  11930  prodmodclem2a  11931  fprodseq  11938  fprodmul  11946  fprodfac  11970  fprodconst  11975  fprodap0  11976  fprodap0f  11991  fprodle  11995  eftcl  12009  ef0lem  12015  efsub  12036  eftlub  12045  eflegeo  12056  tanval2ap  12068  sinadd  12091  cos2t  12105  cos2tsin  12106  sin01bnd  12112  cos01bnd  12113  eirraplem  12132  dvdsval2  12145  dvdsdc  12153  dvds0lem  12156  zdvdsdc  12167  dvdscmulr  12175  dvdsmulcr  12176  fsumdvds  12197  dvdslelemd  12198  divconjdvds  12204  dvdsext  12210  fzm1ndvds  12211  dvdsmod  12217  3dvds  12219  oexpneg  12232  2tp1odd  12239  mulsucdiv2z  12240  2teven  12242  zeo5  12243  opeo  12252  omeo  12253  nn0ob  12263  divalglemnqt  12275  bitsdc  12302  bits0o  12305  bitsfzolem  12309  bitsfzo  12310  bitsmod  12311  bitscmp  12313  bitsinv1lem  12316  gcddvds  12328  dvdslegcd  12329  gcdneg  12347  bezoutlemnewy  12361  bezoutlemstep  12362  bezoutlema  12364  bezoutlemb  12365  bezoutlemmo  12371  bezoutlemle  12373  bezoutlemsup  12374  dfgcd3  12375  bezout  12376  dfgcd2  12379  uzwodc  12402  lcmcllem  12433  lcmneg  12440  lcmgcdlem  12443  lcmdvds  12445  lcmid  12446  3lcm2e6woprm  12452  6lcm4e12  12453  ncoprmgcdne1b  12455  mulgcddvds  12460  divgcdcoprmex  12468  cncongr1  12469  cncongr2  12470  isprm2lem  12482  prmind2  12486  dvdsnprmd  12491  prm2orodd  12492  sqnprm  12502  isprm5lem  12507  rpexp  12519  sqrt2irrlem  12527  oddpwdclemdc  12539  sqrt2irraplemnn  12545  qnumdencoprm  12559  qeqnumdivden  12560  nn0gcdsq  12566  nn0sqrtelqelz  12572  nonsq  12573  phicl2  12580  phibnd  12583  hashdvds  12587  phiprmpw  12588  phimullem  12591  eulerthlemrprm  12595  eulerthlema  12596  eulerthlemth  12598  prmdiveq  12602  hashgcdlem  12604  odzdvds  12612  modprminv  12616  nnnn0modprm0  12622  modprmn0modprm0  12623  pythagtriplem10  12636  pythagtriplem19  12649  pythagtrip  12650  pcpre1  12659  pcpremul  12660  pceu  12662  pcmul  12668  pcdiv  12669  pcqmul  12670  pcqdiv  12674  pcexp  12676  pcdvdsb  12687  pcidlem  12690  pcdvdstr  12694  pcgcd1  12695  pc2dvds  12697  pcprmpw2  12700  difsqpwdvds  12705  pcaddlem  12706  pcadd  12707  pcadd2  12708  pcmpt  12710  pcmptdvds  12712  pcprod  12713  fldivp1  12715  pcfaclem  12716  pcfac  12717  pcbc  12718  qexpz  12719  pockthlem  12723  pockthg  12724  1arithlem4  12733  1arith  12734  1arith2  12735  4sqlem6  12750  4sqlem8  12752  4sqlem9  12753  4sqlem10  12754  4sqexercise1  12765  4sqexercise2  12766  4sqlemsdc  12767  4sqlem11  12768  4sqlem12  12769  4sqlem15  12772  4sqlem16  12773  4sqlem17  12774  znnen  12813  ennnfonelemk  12815  ennnfonelemkh  12827  ennnfonelemhf1o  12828  ennnfonelemrnh  12831  ennnfonelemfun  12832  ennnfonelemf1  12833  ennnfonelemrn  12834  ennnfonelemnn0  12837  ctinfomlemom  12842  ctiunctlemudc  12852  unct  12857  omctfn  12858  ssnnctlemct  12861  nninfdclemp1  12865  nninfdc  12868  structfung  12893  setsfun  12911  setsfun0  12912  setscom  12916  strslfv3  12922  setsslid  12927  pwsdiagel  13173  pwssnf1o  13174  imasaddfnlemg  13190  imasaddvallemg  13191  mgmsscl  13237  plusffng  13241  mgmplusf  13242  mgm0  13245  mgm1  13246  opifismgmdc  13247  gsumfzval  13267  gsumprval  13275  sgrp1  13287  issgrpd  13288  prdsplusgsgrpcl  13290  mndpfo  13314  mndfo  13315  prdsplusgcl  13322  prdsidlem  13323  mnd1  13331  0subm  13360  mhmima  13367  grpinvfng  13420  isgrpinv  13430  grpinvid  13436  grpinvf1o  13446  grpinvadd  13454  grpsubf  13455  grpsubsub4  13469  grplactcnv  13478  grp1  13482  grp1inv  13483  prdsinvlem  13484  prdsinvgd  13486  qusgrp2  13493  mulgfng  13504  subginv  13561  resgrpisgrp  13575  subgintm  13578  0subg  13579  0nsg  13594  qusinv  13616  ghminv  13630  ghmrn  13637  ghmeql  13647  ghmnsgima  13648  kerf1ghm  13654  conjnmz  13659  rngass  13745  rngmneg1  13753  rngmneg2  13754  qusrng  13764  srgideu  13778  srgidmlem  13784  srgpcomp  13796  srg1expzeq1  13801  ringcl  13819  ringideu  13823  ringidmlem  13828  ringnegl  13857  ringnegr  13858  ring1  13865  qusring2  13872  opprringbg  13886  dvdsrd  13900  dvdsr01  13910  isunitd  13912  unitinvcl  13929  unitinvinv  13930  unitnegcl  13936  rhmmul  13970  rhmf1o  13974  nzrunit  13994  lringuplu  14002  subrngintm  14018  subrgsubm  14040  subrgintm  14049  aprsym  14090  scaffng  14115  lmodscaf  14116  lsssn0  14176  lss1d  14189  lssintclm  14190  lspval  14196  lspcl  14197  lspsnid  14213  lspprid1  14217  lspsn  14222  sraval  14243  rspcl  14297  rspssid  14298  rspssp  14300  rnglidlmmgm  14302  rnglidlmsgrp  14303  cnfldneg  14379  zringinvg  14410  expghmap  14413  znzrhfo  14454  znf1o  14457  znhash  14462  znidomb  14464  znrrg  14466  psrbagfi  14479  psraddcl  14486  psr0cl  14487  psrnegcl  14489  psrneg  14493  psr1clfi  14494  mplsubgfilemm  14504  mplsubgfilemcl  14505  baspartn  14566  eltg3i  14572  tgclb  14581  topbas  14583  2basgeng  14598  topcld  14625  0cld  14628  uncld  14629  neif  14657  elnei  14668  0nei  14682  restbasg  14684  iscnp4  14734  cnpnei  14735  cnclima  14739  cncnp  14746  cnrest2r  14753  cndis  14757  lmff  14765  lmtopcnp  14766  txbas  14774  txopn  14781  txcnp  14787  upxp  14788  txdis1cn  14794  cnmpt11  14799  cnmpt21  14807  psmetge0  14847  xmetge0  14881  xmettpos  14886  xmetrtri  14892  metrtri  14893  xblpnfps  14914  xblpnf  14915  blfps  14925  blf  14926  ssblps  14941  ssbl  14942  blbas  14949  metss2  15014  xmettxlem  15025  xmettx  15026  qtopbas  15038  divcnap  15081  cncfss  15099  cdivcncfap  15120  expcncf  15125  cnopnap  15127  maxcncf  15131  mincncf  15132  dedekindeulemuub  15133  dedekindeulemlu  15137  dedekindeu  15139  suplociccex  15141  dedekindicclemuub  15142  dedekindicclemlu  15146  dedekindicclemicc  15148  ivthinclemlopn  15152  ivthinclemuopn  15154  ivthinc  15159  ivthreinc  15161  hoverlt1  15165  ellimc3apf  15176  limcimolemlt  15180  limcimo  15181  limcresi  15182  cnplimclemle  15184  reldvg  15195  dvfgg  15204  dvidlemap  15207  dvidrelem  15208  dvidsslem  15209  dvcjbr  15224  dvcj  15225  dvrecap  15229  dveflem  15242  dvef  15243  elply2  15251  elplyr  15256  plycj  15277  plyreres  15280  reeff1oleme  15288  pilem3  15299  sinq34lt0t  15347  cosq14gt0  15348  coseq0q4123  15350  tangtx  15354  sincosq1eq  15355  cosordlem  15365  logdivlti  15397  relogbval  15467  relogbzcl  15468  nnlogbexp  15475  logbgcd1irr  15483  logbgcd1irraplemexp  15484  logbgcd1irraplemap  15485  wilthlem1  15496  mpodvdsmulf1o  15506  mersenne  15513  perfectlem2  15516  perfect  15517  zabsle1  15520  lgslem1  15521  lgsval  15525  lgsfvalg  15526  lgsfcl2  15527  lgsval2lem  15531  lgscl1  15544  lgsmod  15547  lgsdir2lem5  15553  lgsdir2  15554  lgsdilem2  15557  lgsdi  15558  lgsne0  15559  gausslemma2dlem0c  15572  gausslemma2dlem0h  15577  gausslemma2dlem1a  15579  gausslemma2dlem1f1o  15581  gausslemma2dlem3  15584  lgseisenlem1  15591  lgseisenlem2  15592  lgseisenlem3  15593  lgseisenlem4  15594  lgseisen  15595  lgsquadlem1  15598  lgsquadlem2  15599  lgsquadlem3  15600  lgsquad3  15605  2lgslem3b1  15619  2lgslem3c1  15620  2lgs  15625  2lgsoddprmlem2  15627  2lgsoddprm  15634  2sqlem3  15638  2sqlem8  15644  2sqlem10  15646  structgrssvtx  15685  structgrssiedg  15686  ushgruhgr  15720  uhgrun  15726  incistruhgr  15730  fnmptd  15814  bj-sels  15924  bj-nnelon  15969  2omap  16006  pwle2  16009  pwf1oexmid  16010  pw1nct  16014  nninfall  16020  nninfsellemdc  16021  nninfself  16024  nnnninfex  16033  nninfnfiinf  16034  refeq  16041  isomninnlem  16043  cvgcmp2nlemabs  16045  trilpolemlt1  16054  trirec0  16057  apdifflemf  16059  apdifflemr  16060  apdiff  16061  iswomninnlem  16062  iswomni0  16064  ismkvnnlem  16065  reap0  16071  cndcap  16072