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  940  mpbi2and  946  bilukdc  1416  equs5or  1854  eqtrd  2239  eleqtrd  2285  neeqtrd  2405  3netr3d  2409  rexlimd2  2622  raleqtrdv  2711  rexeqtrdv  2712  ceqsalt  2800  vtoclgft  2825  vtoclegft  2849  elrab3t  2932  eueq2dc  2950  sbceq1dd  3008  csbiedf  3138  sseqtrd  3235  3sstr3d  3241  ifbothdadc  3609  snssd  3784  dfnfc2  3877  breqdi  4069  breqtrd  4080  3brtr3d  4085  csbexga  4183  reuhypd  4531  reg2exmidlema  4595  elirr  4602  en2lp  4615  onsucuni2  4625  finds  4661  iota4  5265  iota4an  5266  funimaexglem  5371  fneu  5394  fco2  5457  fssres2  5470  fresin  5471  feu  5475  f1orescnv  5555  resdif  5561  funcocnv2  5564  f1oprg  5584  fvelrnb  5644  fimacnv  5727  f1oresrab  5763  fsn2  5772  xpsng  5773  funopsn  5780  fnressn  5788  fsnunf  5802  foeqcnvco  5877  isores1  5901  isoini2  5906  riota5f  5942  riotass2  5944  riotass  5945  ovmpodxf  6089  uchoice  6241  elopabi  6299  cnvf1o  6329  smores3  6397  tfrlemisucaccv  6429  tfr1onlemsucaccv  6445  tfrcllemsucaccv  6458  rdgon  6490  frecabcl  6503  frecsuclem  6510  nnsucsssuc  6596  nnsucuniel  6599  erref  6658  iserd  6664  swoer  6666  swoord1  6667  swoord2  6668  erth  6684  erthi  6686  eroveu  6731  pmresg  6781  mapsn  6795  fndmeng  6921  xpen  6962  phplem4  6972  phplem4on  6985  fidifsnen  6988  dif1en  6997  dif1enen  6998  fisbth  7001  diffisn  7011  ac6sfi  7016  fimax2gtri  7019  en2eqpr  7025  unsnfidcex  7038  unsnfidcel  7039  prfidceq  7046  fiintim  7049  fidcenumlemrks  7076  elfi2  7095  elfir  7096  fiuni  7101  fifo  7103  eqsupti  7119  supisoti  7133  ordiso2  7158  casef  7211  difinfsnlem  7222  ctmlemr  7231  ctssdccl  7234  enumct  7238  nninfninc  7246  nnnninfeq  7251  nnnninfeq2  7252  enomnilem  7261  exmidomni  7265  fodjum  7269  fodjuomnilemres  7271  mkvprop  7281  enmkvlem  7284  enwomnilem  7292  nninfdcinf  7294  nninfwlpoimlemdc  7300  nninfinfwlpolem  7301  pr1or2  7323  acfun  7345  2omotaplemap  7399  exmidmotap  7403  ccfunen  7406  cc2lem  7408  dfplpq2  7497  ltanqi  7545  ltmnqi  7546  ltaddnq  7550  subhalfnqq  7557  ltbtwnnqq  7558  archnqq  7560  prarloclemarch2  7562  enq0sym  7575  enq0ref  7576  enq0tr  7577  nqnq0pi  7581  nnnq0lem1  7589  distrnq0  7602  prarloclemlt  7636  prarloclemn  7642  prarloclemcalc  7645  genplt2i  7653  addnqprllem  7670  addnqprulem  7671  addlocprlemgt  7677  appdivnq  7706  prmuloc2  7710  ltexprlemopl  7744  ltexprlemopu  7746  ltexprlemru  7755  prplnqu  7763  cauappcvgprlemopl  7789  cauappcvgprlemlol  7790  cauappcvgprlemladdfu  7797  cauappcvgprlemladdrl  7800  cauappcvgprlem1  7802  archrecnq  7806  archrecpr  7807  caucvgprlemk  7808  caucvgprlemnbj  7810  caucvgprlemm  7811  caucvgprlemopl  7812  caucvgprlemlol  7813  caucvgprlemladdfu  7820  caucvgprlemladdrl  7821  caucvgprlem1  7822  caucvgprprlemk  7826  caucvgprprlemnkeqj  7833  caucvgprprlemnbj  7836  caucvgprprlemml  7837  caucvgprprlemmu  7838  caucvgprprlemopl  7840  caucvgprprlemlol  7841  caucvgprprlemopu  7842  caucvgprprlemexbt  7849  caucvgprprlemexb  7850  caucvgprprlem1  7852  caucvgprprlem2  7853  suplocexprlemru  7862  suplocexprlemdisj  7863  suplocexprlemloc  7864  suplocexprlemub  7866  suplocexprlemlub  7867  prsrlem1  7885  addgt0sr  7918  srpospr  7926  prsrriota  7931  caucvgsrlemgt1  7938  caucvgsrlemoffgt1  7942  caucvgsr  7945  mappsrprg  7947  suplocsrlemb  7949  suplocsrlempr  7950  suplocsrlem  7951  recriota  8033  axsuploc  8175  lelttr  8191  ltletr  8192  ltnsymd  8222  lensymd  8224  cnegexlem3  8279  cnegex2  8281  addcanad  8288  addcan2ad  8289  negcon1ad  8408  negne0d  8411  negrebd  8412  subeq0d  8421  subne0ad  8424  neg11d  8425  subcand  8454  subcan2d  8455  ltadd2  8522  ltadd2dd  8525  add20  8577  ltnegcon1d  8628  ltnegcon2d  8629  lenegcon1d  8630  lenegcon2d  8631  subled  8651  lesubd  8652  ltsub23d  8653  ltsub13d  8654  ltadd1dd  8659  ltsub1dd  8660  ltsub2dd  8661  leadd1dd  8662  leadd2dd  8663  lesub1dd  8664  lesub2dd  8665  recexre  8681  apreap  8690  ltmul1a  8694  reapmul1  8698  cru  8705  apreim  8706  mulge0  8722  leltap  8728  negap0d  8734  ltleap  8735  ltapd  8741  ap0gt0  8743  ap0gt0d  8744  mulcanapad  8766  mulcanap2ad  8767  eqnegad  8837  diveqap0d  8900  diveqap1d  8901  divap1d  8904  rec11apd  8914  div11apd  8934  div2subap  8940  recgt0  8953  prodgt0  8955  lemul1a  8961  lemulge12  8970  lt2msq1  8988  lediv12a  8997  recreclt  9003  nn1suc  9085  nnnlt1  9092  nn2ge  9099  nn1gt1  9100  nnrecl  9323  nn0nlt0  9351  elnn0z  9415  nnnle0  9451  nn0negleid  9471  elz2  9474  nn0n0n1ge2b  9482  nnm1ge0  9489  nn0ge0div  9490  zextle  9494  suprzclex  9501  nn0ind-raph  9520  zindd  9521  uzneg  9697  eluzadd  9707  eluzsub  9708  uzm1  9709  uz3m2nn  9724  supminfex  9748  infregelbex  9749  nn01to3  9768  irrmulap  9799  ltrec1d  9869  lerec2d  9870  ledivdivd  9874  divge1  9875  ltmul1dd  9904  ltmul2dd  9905  ltdiv1dd  9906  lediv1dd  9907  ltdiv23d  9909  lediv23d  9910  nn0ledivnn  9919  addlelt  9920  xrlelttr  9958  xrltletr  9959  xaddass2  10022  xltadd1  10028  xlt2add  10032  ixxdisj  10055  icoshftf1o  10143  icodisj  10144  lincmb01cmp  10155  iccf1o  10156  uzsubsubfz  10199  fzdisj  10204  fzopth  10213  fznatpl1  10228  fzsuc2  10231  fzp1disj  10232  fzrev2i  10238  uzdisj  10245  fseq1p1m1  10246  fzm1  10252  fzneuz  10253  fzp1nel  10256  fzrevral  10257  fznn0sub2  10280  fz0fzdiffz0  10282  difelfzle  10286  difelfznle  10287  nn0disj  10290  fzonnsub  10323  fzodisj  10332  fzouzdisj  10334  fzoun  10335  eluzgtdifelfzo  10358  ubmelfzo  10361  fzonn0p1p1  10374  ubmelm1fzo  10387  fzostep1  10398  exfzdc  10401  subfzo0  10403  zsupcllemstep  10404  infssuzex  10408  zsupssdc  10413  qtri3or  10415  exbtwnzlemex  10424  rebtwn2z  10429  qbtwnrelemcalc  10430  qbtwnre  10431  qavgle  10433  apbtwnz  10449  flid  10459  flqwordi  10463  flqmulnn0  10474  flhalf  10477  flltdivnn0lt  10479  fldiv4p1lem1div2  10480  intfracq  10497  flqdiv  10498  flqpmodeq  10504  modqmulnn  10519  mulqaddmodid  10541  modqmuladdim  10544  modqmuladdnn0  10545  m1modge3gt1  10548  q2submod  10562  modaddmodup  10564  modqsubdir  10570  modqeqmodmin  10571  modfzo0difsn  10572  uzennn  10613  uzsinds  10621  monoord2  10663  ser3mono  10664  iseqf1olemqcl  10676  iseqf1olemnab  10678  iseqf1olemab  10679  iseqf1olemqf1o  10683  iseqf1olemqk  10684  seq3f1olemqsumkj  10688  seq3f1olemqsumk  10689  seq3f1olemqsum  10690  seq3f1olemp  10692  seqf1oglem1  10696  seqf1oglem2  10697  ser3le  10714  exp3val  10718  expnegap0  10724  expgt1  10754  ltexp2a  10768  le2sq2  10792  nnlesq  10820  qsqeqor  10827  bernneq  10837  expnbnd  10840  expnlbnd  10841  expnlbnd2  10842  expeq0d  10846  sq11d  10883  nn0ltexp2  10886  expcand  10894  nn0opthd  10899  facdiv  10915  faclbnd6  10921  facubnd  10922  facavg  10923  bcval4  10929  bcp1nk  10939  bcval5  10940  bcpasc  10943  hashennnuni  10956  isfinite4im  10969  hashnncl  10972  hashunlem  10981  fiprsshashgt1  10994  hashfzp1  11001  zfz1isolemiso  11016  seq3coll  11019  hash2en  11020  iswrdiz  11033  wrdffz  11047  ccatval21sw  11094  ccatass  11097  swrdf  11141  swrdlend  11144  ccatswrd  11156  swrdccat2  11157  pfxsuffeqwrdeq  11184  ccatpfx  11187  ccats1pfxeq  11200  cats1un  11207  wrdind  11208  wrd2ind  11209  seq3shft  11234  cjth  11242  cjdivap  11305  cjne0d  11343  cjap0d  11344  cvg1nlemcxze  11378  cvg1nlemcau  11380  cvg1nlemres  11381  recvguniq  11391  resqrexlemover  11406  resqrexlemdecn  11408  resqrexlemlo  11409  resqrexlemcalc2  11411  resqrexlemcalc3  11412  resqrexlemnmsq  11413  resqrexlemnm  11414  resqrexlemcvg  11415  resqrexlemglsq  11418  resqrexlemga  11419  leabs  11470  absrele  11479  nn0abscl  11481  ltabs  11483  abslt  11484  absle  11485  abstri  11500  amgm2  11514  sqr11d  11569  abs00d  11582  maxabsle  11600  maxabslemlub  11603  maxleastlt  11611  maxltsup  11614  2zsupmax  11622  minmax  11626  2zinfmin  11639  xrmaxleim  11640  xrmaxiflemlub  11644  xrmaxiflemcom  11645  xrmaxiflemval  11646  xrmaxleastlt  11652  xrmaxltsup  11654  xrmaxaddlem  11656  xrmaxadd  11657  xrminmax  11661  xrmin1inf  11663  xrmin2inf  11664  xrmineqinf  11665  climi  11683  reccn2ap  11709  climge0  11721  climle  11730  climserle  11741  climrecvg1n  11744  fz1f1o  11771  summodclem3  11776  summodclem2a  11777  summodc  11779  fisumss  11788  fsum0diaglem  11836  mptfzshft  11838  fsumrev  11839  fisum0diag2  11843  fsumlessfi  11856  fsumle  11859  fsumlt  11860  isumsplit  11887  isumrpcl  11890  expcnvap0  11898  geosergap  11902  pwm1geoserap1  11904  absgtap  11906  geolim  11907  geolim2  11908  georeclim  11909  geoisumr  11914  geoisum1c  11916  cvgratnnlembern  11919  cvgratnnlemseq  11922  cvgratnnlemsumlt  11924  cvgratnnlemfm  11925  cvgratnnlemrate  11926  cvgratnn  11927  cvgratz  11928  mertenslemub  11930  mertenslemi1  11931  mertenslem2  11932  mertensabs  11933  prodmodclem2a  11972  prodmodc  11974  zproddc  11975  fprodntrivap  11980  fprodf1o  11984  fprodssdc  11986  fprodsplitdc  11992  fprodrev  12015  fprodmodd  12037  efcllemp  12054  ege2le3  12067  eftlcvg  12083  eftlub  12086  efltim  12094  eflegeo  12097  tanaddap  12135  sinbnd  12148  cosbnd  12149  sin01bnd  12153  cos01bnd  12154  sinltxirr  12157  sin01gt0  12158  cos01gt0  12159  cos12dec  12164  eirraplem  12173  zdvdsdc  12208  dvdstr  12224  dvdsadd2b  12236  fsumdvds  12238  dvdslelemd  12239  divconjdvds  12245  alzdvds  12250  dvdsext  12251  fzm1ndvds  12252  fzo0dvdseq  12253  3dvds  12260  zeo3  12264  even2n  12270  mod2eq1n2dvds  12275  nn0ehalf  12299  nnehalf  12300  nno  12302  nn0oddm1d2  12305  divalglemnqt  12316  divalglemex  12318  divalglemeuneg  12319  divalg2  12322  divalgmod  12323  flodddiv4t2lthalf  12335  bitsfzolem  12350  bitsfzo  12351  bitsmod  12352  bitsfi  12353  bitscmp  12354  bitsinv1lem  12357  bitsinv1  12358  dvdsbnd  12362  gcdsupex  12363  gcdsupcl  12364  gcddvds  12369  divgcdz  12377  divgcdnn  12381  gcd0id  12385  gcdneg  12388  gcd1  12393  dvdsgcdidd  12400  bezoutlemnewy  12402  bezoutlemstep  12403  bezoutlemmo  12412  bezoutlemsup  12415  dfgcd3  12416  bezout  12417  dfgcd2  12420  mulgcd  12422  sqgcd  12435  dvdssqlem  12436  bezoutr1  12439  uzwodc  12443  nninfctlemfo  12446  lcmval  12470  lcmcllem  12474  dvdslcm  12476  lcmgcdlem  12484  lcmdvds  12486  lcmgcdeq  12490  ncoprmgcdne1b  12496  mulgcddvds  12501  rpmulgcd2  12502  qredeu  12504  rpdvds  12506  prmind2  12527  nprm  12530  dvdsnprmd  12532  isprm5lem  12548  isprm5  12549  divgcdodd  12550  isprm6  12554  prmexpb  12558  pw2dvds  12573  pw2dvdseulemle  12574  oddpwdclemdc  12580  sqne2sq  12584  znege1  12585  sqrt2irraplemnn  12586  divnumden  12603  divdenle  12604  qden1elz  12612  nn0sqrtelqelz  12613  hashdvds  12628  crth  12631  phimullem  12632  eulerthlemfi  12635  eulerthlemh  12638  eulerthlemth  12639  eulerth  12640  prmdiv  12642  prmdiveq  12643  hashgcdlem  12645  dvdsfi  12646  phisum  12648  odzcllem  12650  odzdvds  12653  odzphi  12654  oddprm  12667  pythagtriplem3  12675  pythagtriplem4  12676  pythagtriplem10  12677  pythagtriplem11  12682  pythagtriplem13  12684  pythagtriplem19  12690  pcprendvds  12698  pcprendvds2  12699  pcpre1  12700  pcpremul  12701  pceulem  12702  pceu  12703  pczpre  12705  pcmul  12709  pcdiv  12710  pcqmul  12711  pcqdiv  12715  pcexp  12717  pcidlem  12731  pcneg  12733  pcdvdstr  12735  pcgcd1  12736  pc2dvds  12738  dvdsprmpweq  12743  dvdsprmpweqle  12745  pcaddlem  12747  pcadd  12748  pcadd2  12749  pcmpt  12751  fldivp1  12756  pcfaclem  12757  pcfac  12758  pcbc  12759  qexpz  12760  oddprmdvds  12762  pockthlem  12764  pockthg  12765  infpnlem2  12768  1arith  12775  4sqlem9  12794  4sqlem10  12795  4sqlem11  12809  4sqlem12  12810  4sqlem13m  12811  4sqlem14  12812  4sqlem16  12814  oddennn  12848  ennnfonelemk  12856  ennnfonelemkh  12868  ennnfonelemhf1o  12869  ennnfonelemex  12870  ennnfonelemhom  12871  ennnfonelemrnh  12872  ennnfonelemen  12877  ennnfonelemim  12880  ctinfomlemom  12883  ctiunctlemf  12894  ssnnctlemct  12902  nninfdclemcl  12904  nninfdclemp1  12906  nninfdclemlt  12907  unbendc  12910  prdsbascl  13206  pwselbas  13211  mgmb1mgm1  13285  mgm1  13287  mgmidsssn0  13301  gsumfzval  13308  gsumress  13312  gsum0g  13313  gsumval2  13314  sgrp1  13328  sgrpidmndm  13337  ismndd  13354  prds0g  13366  mhmpropd  13383  resmhm  13404  resmhm2b  13406  gsumwsubmcl  13413  gsumwmhm  13415  isgrpd2e  13437  grpidd2  13458  isgrpinv  13471  grpinvinv  13484  grpidssd  13493  grpinvssd  13494  mulgval  13543  mulgfng  13545  mulgnegnn  13553  subg0  13601  issubg4m  13614  nsgconj  13627  1nsgtrivd  13640  eqgen  13648  eqgcpbl  13649  qus0  13656  ghmid  13670  resghm  13681  ghmnsgpreima  13690  kerf1ghm  13695  conjsubgen  13699  conjnmz  13700  imasabl  13757  rnglz  13792  rngrz  13793  qusrng  13805  issrgid  13828  srg1zr  13834  ringcl  13860  isringid  13872  ringcom  13878  ringpropd  13885  ringlz  13890  ringrz  13891  ring1  13906  opprrng  13924  opprring  13926  dvdsrcld  13944  unitcld  13955  unitmulcl  13960  unitgrp  13963  unitnegcl  13977  rhmmul  14011  isrhm2d  14012  rhmdvdsr  14022  rhmopp  14023  elrhmunit  14024  rhmunitinv  14025  subrgugrp  14087  aprsym  14131  islmodd  14140  lmod0vs  14168  lmodfopne  14173  lmodcom  14180  lssclg  14211  lspsnel5a  14257  lspsneq0b  14274  lsslsp  14276  sraring  14296  sralmod  14297  rspssp  14341  rnglidlmsgrp  14344  2idlcpblrng  14370  gsumfzfsumlem0  14433  zncrng  14492  znzrh2  14493  znzrhfo  14495  znf1o  14498  znfi  14502  znhash  14503  znidom  14504  znidomb  14505  znunit  14506  znrrg  14507  psrbaglesuppg  14519  psrelbas  14522  psrelbasfi  14523  psrgrp  14532  psr0  14533  psr1clfi  14535  mplsubgfilemcl  14546  mplsubgfileminv  14547  ntridm  14683  ntrtop  14685  ntrcls0  14688  ntr0  14691  isopn3i  14692  neiss2  14699  opnneiss  14715  topssnei  14719  cnpf2  14764  icnpimaex  14768  lmcvg  14774  iscnp4  14775  cncnp  14787  cnptopresti  14795  lmfss  14801  lmtopcnp  14807  hmeores  14872  bldisj  14958  xblss2ps  14961  xblss2  14962  blhalf  14965  blssps  14984  blss  14985  ssblex  14988  blpnfctr  14996  xmetresbl  14997  mopni2  15040  bdxmet  15058  bdbl  15060  xmetxpbl  15065  metcnpi  15072  metcnpi2  15073  tgioo  15111  rescncf  15138  mulcncflem  15164  cnopnap  15168  dedekindeulemuub  15174  dedekindeulemloc  15176  dedekindeulemlu  15178  dedekindeu  15180  dedekindicclemuub  15183  dedekindicclemloc  15185  dedekindicclemlu  15187  dedekindicclemicc  15189  dedekindicc  15190  ivthinclemlopn  15193  ivthinclemuopn  15195  ivthdec  15201  ivthreinc  15202  hovergt0  15207  dich0  15209  limcimolemlt  15221  cnplimcim  15224  cnplimclemr  15226  limccnpcntop  15232  limccnp2cntop  15234  limccoap  15235  dvfgg  15245  dvidlemap  15248  dvidrelem  15249  dvidsslem  15250  dvaddxxbr  15258  dvmulxxbr  15259  dvaddxx  15260  dvmulxx  15261  dviaddf  15262  dvimulf  15263  dvcoapbr  15264  dvcjbr  15265  dvcj  15266  dvrecap  15270  dvmptclx  15275  dveflem  15283  elply2  15292  plyf  15294  plyaddlem  15306  plymullem  15307  plycoeid3  15314  plyco  15316  plycj  15318  dvply1  15322  dvply2g  15323  reeff1oleme  15329  eflt  15332  sin0pilem1  15338  pilem3  15340  cosq14gt0  15389  coseq0negpitopi  15393  tangtx  15395  coskpi  15405  cosordlem  15406  cosq34lt1  15407  relogef  15421  logrpap0d  15435  rplogcl  15436  logge0  15437  logdivlti  15438  cxplt3  15477  rpabscxpbnd  15497  dvdsppwf1o  15546  fsumdvdsmul  15548  mersenne  15554  perfect1  15555  perfectlem1  15556  perfectlem2  15557  perfect  15558  lgslem1  15562  lgsval  15566  lgsfvalg  15567  lgsval2lem  15572  lgsvalmod  15581  lgsfcl3  15583  lgsmod  15588  lgsdirprm  15596  lgsdir  15597  lgsdilem2  15598  lgsdi  15599  lgsne0  15600  gausslemma2dlem0i  15619  gausslemma2dlem1a  15620  gausslemma2dlem1f1o  15622  gausslemma2dlem3  15625  gausslemma2dlem4  15626  lgseisenlem1  15632  lgseisenlem2  15633  lgseisenlem3  15634  lgseisenlem4  15635  lgseisen  15636  lgsquadlem1  15639  lgsquadlem2  15640  lgsquadlem3  15641  lgsquad2lem1  15643  lgsquad2lem2  15644  lgsquad3  15646  2lgslem1c  15652  2lgsoddprm  15675  2sqlem3  15679  2sqlem4  15680  2sqlem8  15685  lpvtx  15760  umgrnloopvv  15795  umgredgne  15824  bj-charfunr  15915  2omap  16102  pw1map  16104  pwf1oexmid  16108  subctctexmid  16109  domomsubct  16110  pw1nct  16112  nnsf  16114  peano4nninf  16115  nninfsellemeq  16123  nnnninfex  16131  cvgcmp2nlemabs  16143  iooref1o  16145  trilpolemisumle  16149  trilpolemeq1  16151  trilpolemlt1  16152  trirec0  16155  apdifflemf  16157  apdifflemr  16158  apdiff  16159  iswomninnlem  16160  redcwlpo  16166  redc0  16168  reap0  16169  nconstwlpolemgt0  16175  neapmkvlem  16178  ltlenmkv  16181  supfz  16182  inffz  16183