Theorem mpbid 147

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

Hypotheses

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

Assertion

Ref	Expression
mpbid	⊢ (𝜑 → 𝜒)

Proof of Theorem mpbid

Step	Hyp	Ref	Expression
1		mpbid.min	. 2 ⊢ (𝜑 → 𝜓)
2		mpbid.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimpd 144	. 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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbii  148  annimdc  943  mpbi2and  949  bilukdc  1438  equs5or  1876  eqtrd  2262  eleqtrd  2308  neeqtrd  2428  3netr3d  2432  rexlimd2  2646  raleqtrdv  2736  rexeqtrdv  2737  ceqsalt  2826  vtoclgft  2851  vtoclegft  2875  elrab3t  2958  eueq2dc  2976  sbceq1dd  3034  csbiedf  3165  sseqtrd  3262  3sstr3d  3268  ifbothdadc  3636  snssd  3812  dfnfc2  3905  breqdi  4097  breqtrd  4108  3brtr3d  4113  csbexga  4211  reuhypd  4561  reg2exmidlema  4625  elirr  4632  en2lp  4645  onsucuni2  4655  finds  4691  iota4  5297  iota4an  5298  funimaexglem  5403  fneu  5426  fco2  5489  fssres2  5502  fresin  5503  feu  5507  f1orescnv  5587  resdif  5593  funcocnv2  5596  f1oprg  5616  fvelrnb  5680  fimacnv  5763  f1oresrab  5799  fsn2  5808  xpsng  5809  funopsn  5816  fnressn  5824  fsnunf  5838  foeqcnvco  5913  isores1  5937  isoini2  5942  riota5f  5980  riotass2  5982  riotass  5983  ovmpodxf  6129  uchoice  6281  elopabi  6339  cnvf1o  6369  smores3  6437  tfrlemisucaccv  6469  tfr1onlemsucaccv  6485  tfrcllemsucaccv  6498  rdgon  6530  frecabcl  6543  frecsuclem  6550  nnsucsssuc  6636  nnsucuniel  6639  erref  6698  iserd  6704  swoer  6706  swoord1  6707  swoord2  6708  erth  6724  erthi  6726  eroveu  6771  pmresg  6821  mapsn  6835  fndmeng  6961  xpen  7002  phplem4  7012  phplem4on  7025  fidifsnen  7028  dif1en  7037  dif1enen  7038  fisbth  7041  diffisn  7051  ac6sfi  7056  fimax2gtri  7059  en2eqpr  7065  unsnfidcex  7078  unsnfidcel  7079  prfidceq  7086  fiintim  7089  fidcenumlemrks  7116  elfi2  7135  elfir  7136  fiuni  7141  fifo  7143  eqsupti  7159  supisoti  7173  ordiso2  7198  casef  7251  difinfsnlem  7262  ctmlemr  7271  ctssdccl  7274  enumct  7278  nninfninc  7286  nnnninfeq  7291  nnnninfeq2  7292  enomnilem  7301  exmidomni  7305  fodjum  7309  fodjuomnilemres  7311  mkvprop  7321  enmkvlem  7324  enwomnilem  7332  nninfdcinf  7334  nninfwlpoimlemdc  7340  nninfinfwlpolem  7341  pr1or2  7363  acfun  7385  2omotaplemap  7439  exmidmotap  7443  ccfunen  7446  cc2lem  7448  dfplpq2  7537  ltanqi  7585  ltmnqi  7586  ltaddnq  7590  subhalfnqq  7597  ltbtwnnqq  7598  archnqq  7600  prarloclemarch2  7602  enq0sym  7615  enq0ref  7616  enq0tr  7617  nqnq0pi  7621  nnnq0lem1  7629  distrnq0  7642  prarloclemlt  7676  prarloclemn  7682  prarloclemcalc  7685  genplt2i  7693  addnqprllem  7710  addnqprulem  7711  addlocprlemgt  7717  appdivnq  7746  prmuloc2  7750  ltexprlemopl  7784  ltexprlemopu  7786  ltexprlemru  7795  prplnqu  7803  cauappcvgprlemopl  7829  cauappcvgprlemlol  7830  cauappcvgprlemladdfu  7837  cauappcvgprlemladdrl  7840  cauappcvgprlem1  7842  archrecnq  7846  archrecpr  7847  caucvgprlemk  7848  caucvgprlemnbj  7850  caucvgprlemm  7851  caucvgprlemopl  7852  caucvgprlemlol  7853  caucvgprlemladdfu  7860  caucvgprlemladdrl  7861  caucvgprlem1  7862  caucvgprprlemk  7866  caucvgprprlemnkeqj  7873  caucvgprprlemnbj  7876  caucvgprprlemml  7877  caucvgprprlemmu  7878  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemopu  7882  caucvgprprlemexbt  7889  caucvgprprlemexb  7890  caucvgprprlem1  7892  caucvgprprlem2  7893  suplocexprlemru  7902  suplocexprlemdisj  7903  suplocexprlemloc  7904  suplocexprlemub  7906  suplocexprlemlub  7907  prsrlem1  7925  addgt0sr  7958  srpospr  7966  prsrriota  7971  caucvgsrlemgt1  7978  caucvgsrlemoffgt1  7982  caucvgsr  7985  mappsrprg  7987  suplocsrlemb  7989  suplocsrlempr  7990  suplocsrlem  7991  recriota  8073  axsuploc  8215  lelttr  8231  ltletr  8232  ltnsymd  8262  lensymd  8264  cnegexlem3  8319  cnegex2  8321  addcanad  8328  addcan2ad  8329  negcon1ad  8448  negne0d  8451  negrebd  8452  subeq0d  8461  subne0ad  8464  neg11d  8465  subcand  8494  subcan2d  8495  ltadd2  8562  ltadd2dd  8565  add20  8617  ltnegcon1d  8668  ltnegcon2d  8669  lenegcon1d  8670  lenegcon2d  8671  subled  8691  lesubd  8692  ltsub23d  8693  ltsub13d  8694  ltadd1dd  8699  ltsub1dd  8700  ltsub2dd  8701  leadd1dd  8702  leadd2dd  8703  lesub1dd  8704  lesub2dd  8705  recexre  8721  apreap  8730  ltmul1a  8734  reapmul1  8738  cru  8745  apreim  8746  mulge0  8762  leltap  8768  negap0d  8774  ltleap  8775  ltapd  8781  ap0gt0  8783  ap0gt0d  8784  mulcanapad  8806  mulcanap2ad  8807  eqnegad  8877  diveqap0d  8940  diveqap1d  8941  divap1d  8944  rec11apd  8954  div11apd  8974  div2subap  8980  recgt0  8993  prodgt0  8995  lemul1a  9001  lemulge12  9010  lt2msq1  9028  lediv12a  9037  recreclt  9043  nn1suc  9125  nnnlt1  9132  nn2ge  9139  nn1gt1  9140  nnrecl  9363  nn0nlt0  9391  elnn0z  9455  nnnle0  9491  nn0negleid  9511  elz2  9514  nn0n0n1ge2b  9522  nnm1ge0  9529  nn0ge0div  9530  zextle  9534  suprzclex  9541  nn0ind-raph  9560  zindd  9561  uzneg  9737  eluzadd  9747  eluzsub  9748  uzm1  9749  uz3m2nn  9764  supminfex  9788  infregelbex  9789  nn01to3  9808  irrmulap  9839  ltrec1d  9909  lerec2d  9910  ledivdivd  9914  divge1  9915  ltmul1dd  9944  ltmul2dd  9945  ltdiv1dd  9946  lediv1dd  9947  ltdiv23d  9949  lediv23d  9950  nn0ledivnn  9959  addlelt  9960  xrlelttr  9998  xrltletr  9999  xaddass2  10062  xltadd1  10068  xlt2add  10072  ixxdisj  10095  icoshftf1o  10183  icodisj  10184  lincmb01cmp  10195  iccf1o  10196  uzsubsubfz  10239  fzdisj  10244  fzopth  10253  fznatpl1  10268  fzsuc2  10271  fzp1disj  10272  fzrev2i  10278  uzdisj  10285  fseq1p1m1  10286  fzm1  10292  fzneuz  10293  fzp1nel  10296  fzrevral  10297  fznn0sub2  10320  fz0fzdiffz0  10322  difelfzle  10326  difelfznle  10327  nn0disj  10330  fzonnsub  10363  fzodisj  10372  fzouzdisj  10374  fzoun  10375  eluzgtdifelfzo  10398  ubmelfzo  10401  fzonn0p1p1  10414  ubmelm1fzo  10427  fzostep1  10438  exfzdc  10441  subfzo0  10443  zsupcllemstep  10444  infssuzex  10448  zsupssdc  10453  qtri3or  10455  exbtwnzlemex  10464  rebtwn2z  10469  qbtwnrelemcalc  10470  qbtwnre  10471  qavgle  10473  apbtwnz  10489  flid  10499  flqwordi  10503  flqmulnn0  10514  flhalf  10517  flltdivnn0lt  10519  fldiv4p1lem1div2  10520  intfracq  10537  flqdiv  10538  flqpmodeq  10544  modqmulnn  10559  mulqaddmodid  10581  modqmuladdim  10584  modqmuladdnn0  10585  m1modge3gt1  10588  q2submod  10602  modaddmodup  10604  modqsubdir  10610  modqeqmodmin  10611  modfzo0difsn  10612  uzennn  10653  uzsinds  10661  monoord2  10703  ser3mono  10704  iseqf1olemqcl  10716  iseqf1olemnab  10718  iseqf1olemab  10719  iseqf1olemqf1o  10723  iseqf1olemqk  10724  seq3f1olemqsumkj  10728  seq3f1olemqsumk  10729  seq3f1olemqsum  10730  seq3f1olemp  10732  seqf1oglem1  10736  seqf1oglem2  10737  ser3le  10754  exp3val  10758  expnegap0  10764  expgt1  10794  ltexp2a  10808  le2sq2  10832  nnlesq  10860  qsqeqor  10867  bernneq  10877  expnbnd  10880  expnlbnd  10881  expnlbnd2  10882  expeq0d  10886  sq11d  10923  nn0ltexp2  10926  expcand  10934  nn0opthd  10939  facdiv  10955  faclbnd6  10961  facubnd  10962  facavg  10963  bcval4  10969  bcp1nk  10979  bcval5  10980  bcpasc  10983  hashennnuni  10996  isfinite4im  11009  hashnncl  11012  hashunlem  11021  fiprsshashgt1  11034  hashfzp1  11041  zfz1isolemiso  11056  seq3coll  11059  hash2en  11060  iswrdiz  11073  wrdffz  11087  ffz0iswrdnn0  11093  ccatval21sw  11135  ccatass  11138  swrdf  11182  swrdlend  11185  ccatswrd  11197  swrdccat2  11198  pfxsuffeqwrdeq  11225  ccatpfx  11228  ccats1pfxeq  11241  cats1un  11248  wrdind  11249  wrd2ind  11250  pfxccatin12  11260  swrdccat  11262  s2dmg  11317  seq3shft  11344  cjth  11352  cjdivap  11415  cjne0d  11453  cjap0d  11454  cvg1nlemcxze  11488  cvg1nlemcau  11490  cvg1nlemres  11491  recvguniq  11501  resqrexlemover  11516  resqrexlemdecn  11518  resqrexlemlo  11519  resqrexlemcalc2  11521  resqrexlemcalc3  11522  resqrexlemnmsq  11523  resqrexlemnm  11524  resqrexlemcvg  11525  resqrexlemglsq  11528  resqrexlemga  11529  leabs  11580  absrele  11589  nn0abscl  11591  ltabs  11593  abslt  11594  absle  11595  abstri  11610  amgm2  11624  sqr11d  11679  abs00d  11692  maxabsle  11710  maxabslemlub  11713  maxleastlt  11721  maxltsup  11724  2zsupmax  11732  minmax  11736  2zinfmin  11749  xrmaxleim  11750  xrmaxiflemlub  11754  xrmaxiflemcom  11755  xrmaxiflemval  11756  xrmaxleastlt  11762  xrmaxltsup  11764  xrmaxaddlem  11766  xrmaxadd  11767  xrminmax  11771  xrmin1inf  11773  xrmin2inf  11774  xrmineqinf  11775  climi  11793  reccn2ap  11819  climge0  11831  climle  11840  climserle  11851  climrecvg1n  11854  fz1f1o  11881  summodclem3  11886  summodclem2a  11887  summodc  11889  fisumss  11898  fsum0diaglem  11946  mptfzshft  11948  fsumrev  11949  fisum0diag2  11953  fsumlessfi  11966  fsumle  11969  fsumlt  11970  isumsplit  11997  isumrpcl  12000  expcnvap0  12008  geosergap  12012  pwm1geoserap1  12014  absgtap  12016  geolim  12017  geolim2  12018  georeclim  12019  geoisumr  12024  geoisum1c  12026  cvgratnnlembern  12029  cvgratnnlemseq  12032  cvgratnnlemsumlt  12034  cvgratnnlemfm  12035  cvgratnnlemrate  12036  cvgratnn  12037  cvgratz  12038  mertenslemub  12040  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  prodmodclem2a  12082  prodmodc  12084  zproddc  12085  fprodntrivap  12090  fprodf1o  12094  fprodssdc  12096  fprodsplitdc  12102  fprodrev  12125  fprodmodd  12147  efcllemp  12164  ege2le3  12177  eftlcvg  12193  eftlub  12196  efltim  12204  eflegeo  12207  tanaddap  12245  sinbnd  12258  cosbnd  12259  sin01bnd  12263  cos01bnd  12264  sinltxirr  12267  sin01gt0  12268  cos01gt0  12269  cos12dec  12274  eirraplem  12283  zdvdsdc  12318  dvdstr  12334  dvdsadd2b  12346  fsumdvds  12348  dvdslelemd  12349  divconjdvds  12355  alzdvds  12360  dvdsext  12361  fzm1ndvds  12362  fzo0dvdseq  12363  3dvds  12370  zeo3  12374  even2n  12380  mod2eq1n2dvds  12385  nn0ehalf  12409  nnehalf  12410  nno  12412  nn0oddm1d2  12415  divalglemnqt  12426  divalglemex  12428  divalglemeuneg  12429  divalg2  12432  divalgmod  12433  flodddiv4t2lthalf  12445  bitsfzolem  12460  bitsfzo  12461  bitsmod  12462  bitsfi  12463  bitscmp  12464  bitsinv1lem  12467  bitsinv1  12468  dvdsbnd  12472  gcdsupex  12473  gcdsupcl  12474  gcddvds  12479  divgcdz  12487  divgcdnn  12491  gcd0id  12495  gcdneg  12498  gcd1  12503  dvdsgcdidd  12510  bezoutlemnewy  12512  bezoutlemstep  12513  bezoutlemmo  12522  bezoutlemsup  12525  dfgcd3  12526  bezout  12527  dfgcd2  12530  mulgcd  12532  sqgcd  12545  dvdssqlem  12546  bezoutr1  12549  uzwodc  12553  nninfctlemfo  12556  lcmval  12580  lcmcllem  12584  dvdslcm  12586  lcmgcdlem  12594  lcmdvds  12596  lcmgcdeq  12600  ncoprmgcdne1b  12606  mulgcddvds  12611  rpmulgcd2  12612  qredeu  12614  rpdvds  12616  prmind2  12637  nprm  12640  dvdsnprmd  12642  isprm5lem  12658  isprm5  12659  divgcdodd  12660  isprm6  12664  prmexpb  12668  pw2dvds  12683  pw2dvdseulemle  12684  oddpwdclemdc  12690  sqne2sq  12694  znege1  12695  sqrt2irraplemnn  12696  divnumden  12713  divdenle  12714  qden1elz  12722  nn0sqrtelqelz  12723  hashdvds  12738  crth  12741  phimullem  12742  eulerthlemfi  12745  eulerthlemh  12748  eulerthlemth  12749  eulerth  12750  prmdiv  12752  prmdiveq  12753  hashgcdlem  12755  dvdsfi  12756  phisum  12758  odzcllem  12760  odzdvds  12763  odzphi  12764  oddprm  12777  pythagtriplem3  12785  pythagtriplem4  12786  pythagtriplem10  12787  pythagtriplem11  12792  pythagtriplem13  12794  pythagtriplem19  12800  pcprendvds  12808  pcprendvds2  12809  pcpre1  12810  pcpremul  12811  pceulem  12812  pceu  12813  pczpre  12815  pcmul  12819  pcdiv  12820  pcqmul  12821  pcqdiv  12825  pcexp  12827  pcidlem  12841  pcneg  12843  pcdvdstr  12845  pcgcd1  12846  pc2dvds  12848  dvdsprmpweq  12853  dvdsprmpweqle  12855  pcaddlem  12857  pcadd  12858  pcadd2  12859  pcmpt  12861  fldivp1  12866  pcfaclem  12867  pcfac  12868  pcbc  12869  qexpz  12870  oddprmdvds  12872  pockthlem  12874  pockthg  12875  infpnlem2  12878  1arith  12885  4sqlem9  12904  4sqlem10  12905  4sqlem11  12919  4sqlem12  12920  4sqlem13m  12921  4sqlem14  12922  4sqlem16  12924  oddennn  12958  ennnfonelemk  12966  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemex  12980  ennnfonelemhom  12981  ennnfonelemrnh  12982  ennnfonelemen  12987  ennnfonelemim  12990  ctinfomlemom  12993  ctiunctlemf  13004  ssnnctlemct  13012  nninfdclemcl  13014  nninfdclemp1  13016  nninfdclemlt  13017  unbendc  13020  prdsbascl  13317  pwselbas  13322  mgmb1mgm1  13396  mgm1  13398  mgmidsssn0  13412  gsumfzval  13419  gsumress  13423  gsum0g  13424  gsumval2  13425  sgrp1  13439  sgrpidmndm  13448  ismndd  13465  prds0g  13477  mhmpropd  13494  resmhm  13515  resmhm2b  13517  gsumwsubmcl  13524  gsumwmhm  13526  isgrpd2e  13548  grpidd2  13569  isgrpinv  13582  grpinvinv  13595  grpidssd  13604  grpinvssd  13605  mulgval  13654  mulgfng  13656  mulgnegnn  13664  subg0  13712  issubg4m  13725  nsgconj  13738  1nsgtrivd  13751  eqgen  13759  eqgcpbl  13760  qus0  13767  ghmid  13781  resghm  13792  ghmnsgpreima  13801  kerf1ghm  13806  conjsubgen  13810  conjnmz  13811  imasabl  13868  rnglz  13903  rngrz  13904  qusrng  13916  issrgid  13939  srg1zr  13945  ringcl  13971  isringid  13983  ringcom  13989  ringpropd  13996  ringlz  14001  ringrz  14002  ring1  14017  opprrng  14035  opprring  14037  dvdsrcld  14055  unitcld  14066  unitmulcl  14071  unitgrp  14074  unitnegcl  14088  rhmmul  14122  isrhm2d  14123  rhmdvdsr  14133  rhmopp  14134  elrhmunit  14135  rhmunitinv  14136  subrgugrp  14198  aprsym  14242  islmodd  14251  lmod0vs  14279  lmodfopne  14284  lmodcom  14291  lssclg  14322  lspsnel5a  14368  lspsneq0b  14385  lsslsp  14387  sraring  14407  sralmod  14408  rspssp  14452  rnglidlmsgrp  14455  2idlcpblrng  14481  gsumfzfsumlem0  14544  zncrng  14603  znzrh2  14604  znzrhfo  14606  znf1o  14609  znfi  14613  znhash  14614  znidom  14615  znidomb  14616  znunit  14617  znrrg  14618  psrbaglesuppg  14630  psrelbas  14633  psrelbasfi  14634  psrgrp  14643  psr0  14644  psr1clfi  14646  mplsubgfilemcl  14657  mplsubgfileminv  14658  ntridm  14794  ntrtop  14796  ntrcls0  14799  ntr0  14802  isopn3i  14803  neiss2  14810  opnneiss  14826  topssnei  14830  cnpf2  14875  icnpimaex  14879  lmcvg  14885  iscnp4  14886  cncnp  14898  cnptopresti  14906  lmfss  14912  lmtopcnp  14918  hmeores  14983  bldisj  15069  xblss2ps  15072  xblss2  15073  blhalf  15076  blssps  15095  blss  15096  ssblex  15099  blpnfctr  15107  xmetresbl  15108  mopni2  15151  bdxmet  15169  bdbl  15171  xmetxpbl  15176  metcnpi  15183  metcnpi2  15184  tgioo  15222  rescncf  15249  mulcncflem  15275  cnopnap  15279  dedekindeulemuub  15285  dedekindeulemloc  15287  dedekindeulemlu  15289  dedekindeu  15291  dedekindicclemuub  15294  dedekindicclemloc  15296  dedekindicclemlu  15298  dedekindicclemicc  15300  dedekindicc  15301  ivthinclemlopn  15304  ivthinclemuopn  15306  ivthdec  15312  ivthreinc  15313  hovergt0  15318  dich0  15320  limcimolemlt  15332  cnplimcim  15335  cnplimclemr  15337  limccnpcntop  15343  limccnp2cntop  15345  limccoap  15346  dvfgg  15356  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvaddxxbr  15369  dvmulxxbr  15370  dvaddxx  15371  dvmulxx  15372  dviaddf  15373  dvimulf  15374  dvcoapbr  15375  dvcjbr  15376  dvcj  15377  dvrecap  15381  dvmptclx  15386  dveflem  15394  elply2  15403  plyf  15405  plyaddlem  15417  plymullem  15418  plycoeid3  15425  plyco  15427  plycj  15429  dvply1  15433  dvply2g  15434  reeff1oleme  15440  eflt  15443  sin0pilem1  15449  pilem3  15451  cosq14gt0  15500  coseq0negpitopi  15504  tangtx  15506  coskpi  15516  cosordlem  15517  cosq34lt1  15518  relogef  15532  logrpap0d  15546  rplogcl  15547  logge0  15548  logdivlti  15549  cxplt3  15588  rpabscxpbnd  15608  dvdsppwf1o  15657  fsumdvdsmul  15659  mersenne  15665  perfect1  15666  perfectlem1  15667  perfectlem2  15668  perfect  15669  lgslem1  15673  lgsval  15677  lgsfvalg  15678  lgsval2lem  15683  lgsvalmod  15692  lgsfcl3  15694  lgsmod  15699  lgsdirprm  15707  lgsdir  15708  lgsdilem2  15709  lgsdi  15710  lgsne0  15711  gausslemma2dlem0i  15730  gausslemma2dlem1a  15731  gausslemma2dlem1f1o  15733  gausslemma2dlem3  15736  gausslemma2dlem4  15737  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgseisenlem4  15746  lgseisen  15747  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad2lem1  15754  lgsquad2lem2  15755  lgsquad3  15757  2lgslem1c  15763  2lgsoddprm  15786  2sqlem3  15790  2sqlem4  15791  2sqlem8  15796  lpvtx  15873  umgrnloopv  15908  umgredgne  15942  ausgrusgrien  15963  bj-charfunr  16131  2omap  16318  pw1map  16320  pwf1oexmid  16324  subctctexmid  16325  domomsubct  16326  pw1nct  16328  nnsf  16330  peano4nninf  16331  nninfsellemeq  16339  nnnninfex  16347  cvgcmp2nlemabs  16359  iooref1o  16361  trilpolemisumle  16365  trilpolemeq1  16367  trilpolemlt1  16368  trirec0  16371  apdifflemf  16373  apdifflemr  16374  apdiff  16375  iswomninnlem  16376  redcwlpo  16382  redc0  16384  reap0  16385  nconstwlpolemgt0  16391  neapmkvlem  16394  ltlenmkv  16397  supfz  16398  inffz  16399