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  939  mpbi2and  945  bilukdc  1415  equs5or  1852  eqtrd  2237  eleqtrd  2283  neeqtrd  2403  3netr3d  2407  rexlimd2  2620  raleqtrdv  2709  rexeqtrdv  2710  ceqsalt  2797  vtoclgft  2822  vtoclegft  2844  elrab3t  2927  eueq2dc  2945  sbceq1dd  3003  csbiedf  3133  sseqtrd  3230  3sstr3d  3236  ifbothdadc  3603  snssd  3777  dfnfc2  3867  breqdi  4058  breqtrd  4069  3brtr3d  4074  csbexga  4171  reuhypd  4517  reg2exmidlema  4581  elirr  4588  en2lp  4601  onsucuni2  4611  finds  4647  iota4  5250  iota4an  5251  funimaexglem  5356  fneu  5379  fco2  5441  fssres2  5452  fresin  5453  feu  5457  f1orescnv  5537  resdif  5543  funcocnv2  5546  f1oprg  5565  fvelrnb  5625  fimacnv  5708  f1oresrab  5744  fsn2  5753  xpsng  5754  funopsn  5761  fnressn  5769  fsnunf  5783  foeqcnvco  5858  isores1  5882  isoini2  5887  riota5f  5923  riotass2  5925  riotass  5926  ovmpodxf  6070  uchoice  6222  elopabi  6280  cnvf1o  6310  smores3  6378  tfrlemisucaccv  6410  tfr1onlemsucaccv  6426  tfrcllemsucaccv  6439  rdgon  6471  frecabcl  6484  frecsuclem  6491  nnsucsssuc  6577  nnsucuniel  6580  erref  6639  iserd  6645  swoer  6647  swoord1  6648  swoord2  6649  erth  6665  erthi  6667  eroveu  6712  pmresg  6762  mapsn  6776  fndmeng  6901  xpen  6941  phplem4  6951  phplem4on  6963  fidifsnen  6966  dif1en  6975  dif1enen  6976  fisbth  6979  diffisn  6989  ac6sfi  6994  fimax2gtri  6997  en2eqpr  7003  unsnfidcex  7016  unsnfidcel  7017  prfidceq  7024  fiintim  7027  fidcenumlemrks  7054  elfi2  7073  elfir  7074  fiuni  7079  fifo  7081  eqsupti  7097  supisoti  7111  ordiso2  7136  casef  7189  difinfsnlem  7200  ctmlemr  7209  ctssdccl  7212  enumct  7216  nninfninc  7224  nnnninfeq  7229  nnnninfeq2  7230  enomnilem  7239  exmidomni  7243  fodjum  7247  fodjuomnilemres  7249  mkvprop  7259  enmkvlem  7262  enwomnilem  7270  nninfdcinf  7272  nninfwlpoimlemdc  7278  nninfinfwlpolem  7279  acfun  7318  2omotaplemap  7368  exmidmotap  7372  ccfunen  7375  cc2lem  7377  dfplpq2  7466  ltanqi  7514  ltmnqi  7515  ltaddnq  7519  subhalfnqq  7526  ltbtwnnqq  7527  archnqq  7529  prarloclemarch2  7531  enq0sym  7544  enq0ref  7545  enq0tr  7546  nqnq0pi  7550  nnnq0lem1  7558  distrnq0  7571  prarloclemlt  7605  prarloclemn  7611  prarloclemcalc  7614  genplt2i  7622  addnqprllem  7639  addnqprulem  7640  addlocprlemgt  7646  appdivnq  7675  prmuloc2  7679  ltexprlemopl  7713  ltexprlemopu  7715  ltexprlemru  7724  prplnqu  7732  cauappcvgprlemopl  7758  cauappcvgprlemlol  7759  cauappcvgprlemladdfu  7766  cauappcvgprlemladdrl  7769  cauappcvgprlem1  7771  archrecnq  7775  archrecpr  7776  caucvgprlemk  7777  caucvgprlemnbj  7779  caucvgprlemm  7780  caucvgprlemopl  7781  caucvgprlemlol  7782  caucvgprlemladdfu  7789  caucvgprlemladdrl  7790  caucvgprlem1  7791  caucvgprprlemk  7795  caucvgprprlemnkeqj  7802  caucvgprprlemnbj  7805  caucvgprprlemml  7806  caucvgprprlemmu  7807  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemopu  7811  caucvgprprlemexbt  7818  caucvgprprlemexb  7819  caucvgprprlem1  7821  caucvgprprlem2  7822  suplocexprlemru  7831  suplocexprlemdisj  7832  suplocexprlemloc  7833  suplocexprlemub  7835  suplocexprlemlub  7836  prsrlem1  7854  addgt0sr  7887  srpospr  7895  prsrriota  7900  caucvgsrlemgt1  7907  caucvgsrlemoffgt1  7911  caucvgsr  7914  mappsrprg  7916  suplocsrlemb  7918  suplocsrlempr  7919  suplocsrlem  7920  recriota  8002  axsuploc  8144  lelttr  8160  ltletr  8161  ltnsymd  8191  lensymd  8193  cnegexlem3  8248  cnegex2  8250  addcanad  8257  addcan2ad  8258  negcon1ad  8377  negne0d  8380  negrebd  8381  subeq0d  8390  subne0ad  8393  neg11d  8394  subcand  8423  subcan2d  8424  ltadd2  8491  ltadd2dd  8494  add20  8546  ltnegcon1d  8597  ltnegcon2d  8598  lenegcon1d  8599  lenegcon2d  8600  subled  8620  lesubd  8621  ltsub23d  8622  ltsub13d  8623  ltadd1dd  8628  ltsub1dd  8629  ltsub2dd  8630  leadd1dd  8631  leadd2dd  8632  lesub1dd  8633  lesub2dd  8634  recexre  8650  apreap  8659  ltmul1a  8663  reapmul1  8667  cru  8674  apreim  8675  mulge0  8691  leltap  8697  negap0d  8703  ltleap  8704  ltapd  8710  ap0gt0  8712  ap0gt0d  8713  mulcanapad  8735  mulcanap2ad  8736  eqnegad  8806  diveqap0d  8869  diveqap1d  8870  divap1d  8873  rec11apd  8883  div11apd  8903  div2subap  8909  recgt0  8922  prodgt0  8924  lemul1a  8930  lemulge12  8939  lt2msq1  8957  lediv12a  8966  recreclt  8972  nn1suc  9054  nnnlt1  9061  nn2ge  9068  nn1gt1  9069  nnrecl  9292  nn0nlt0  9320  elnn0z  9384  nnnle0  9420  nn0negleid  9440  elz2  9443  nn0n0n1ge2b  9451  nnm1ge0  9458  nn0ge0div  9459  zextle  9463  suprzclex  9470  nn0ind-raph  9489  zindd  9490  uzneg  9666  eluzadd  9676  eluzsub  9677  uzm1  9678  uz3m2nn  9693  supminfex  9717  infregelbex  9718  nn01to3  9737  irrmulap  9768  ltrec1d  9838  lerec2d  9839  ledivdivd  9843  divge1  9844  ltmul1dd  9873  ltmul2dd  9874  ltdiv1dd  9875  lediv1dd  9876  ltdiv23d  9878  lediv23d  9879  nn0ledivnn  9888  addlelt  9889  xrlelttr  9927  xrltletr  9928  xaddass2  9991  xltadd1  9997  xlt2add  10001  ixxdisj  10024  icoshftf1o  10112  icodisj  10113  lincmb01cmp  10124  iccf1o  10125  uzsubsubfz  10168  fzdisj  10173  fzopth  10182  fznatpl1  10197  fzsuc2  10200  fzp1disj  10201  fzrev2i  10207  uzdisj  10214  fseq1p1m1  10215  fzm1  10221  fzneuz  10222  fzp1nel  10225  fzrevral  10226  fznn0sub2  10249  fz0fzdiffz0  10251  difelfzle  10255  difelfznle  10256  nn0disj  10259  fzonnsub  10291  fzodisj  10300  fzouzdisj  10302  eluzgtdifelfzo  10324  ubmelfzo  10327  fzonn0p1p1  10340  ubmelm1fzo  10353  fzostep1  10364  exfzdc  10367  subfzo0  10369  zsupcllemstep  10370  infssuzex  10374  zsupssdc  10379  qtri3or  10381  exbtwnzlemex  10390  rebtwn2z  10395  qbtwnrelemcalc  10396  qbtwnre  10397  qavgle  10399  apbtwnz  10415  flid  10425  flqwordi  10429  flqmulnn0  10440  flhalf  10443  flltdivnn0lt  10445  fldiv4p1lem1div2  10446  intfracq  10463  flqdiv  10464  flqpmodeq  10470  modqmulnn  10485  mulqaddmodid  10507  modqmuladdim  10510  modqmuladdnn0  10511  m1modge3gt1  10514  q2submod  10528  modaddmodup  10530  modqsubdir  10536  modqeqmodmin  10537  modfzo0difsn  10538  uzennn  10579  uzsinds  10587  monoord2  10629  ser3mono  10630  iseqf1olemqcl  10642  iseqf1olemnab  10644  iseqf1olemab  10645  iseqf1olemqf1o  10649  iseqf1olemqk  10650  seq3f1olemqsumkj  10654  seq3f1olemqsumk  10655  seq3f1olemqsum  10656  seq3f1olemp  10658  seqf1oglem1  10662  seqf1oglem2  10663  ser3le  10680  exp3val  10684  expnegap0  10690  expgt1  10720  ltexp2a  10734  le2sq2  10758  nnlesq  10786  qsqeqor  10793  bernneq  10803  expnbnd  10806  expnlbnd  10807  expnlbnd2  10808  expeq0d  10812  sq11d  10849  nn0ltexp2  10852  expcand  10860  nn0opthd  10865  facdiv  10881  faclbnd6  10887  facubnd  10888  facavg  10889  bcval4  10895  bcp1nk  10905  bcval5  10906  bcpasc  10909  hashennnuni  10922  isfinite4im  10935  hashnncl  10938  hashunlem  10947  fiprsshashgt1  10960  hashfzp1  10967  zfz1isolemiso  10982  seq3coll  10985  hash2en  10986  iswrdiz  10999  wrdffz  11013  ccatval21sw  11059  ccatass  11062  seq3shft  11120  cjth  11128  cjdivap  11191  cjne0d  11229  cjap0d  11230  cvg1nlemcxze  11264  cvg1nlemcau  11266  cvg1nlemres  11267  recvguniq  11277  resqrexlemover  11292  resqrexlemdecn  11294  resqrexlemlo  11295  resqrexlemcalc2  11297  resqrexlemcalc3  11298  resqrexlemnmsq  11299  resqrexlemnm  11300  resqrexlemcvg  11301  resqrexlemglsq  11304  resqrexlemga  11305  leabs  11356  absrele  11365  nn0abscl  11367  ltabs  11369  abslt  11370  absle  11371  abstri  11386  amgm2  11400  sqr11d  11455  abs00d  11468  maxabsle  11486  maxabslemlub  11489  maxleastlt  11497  maxltsup  11500  2zsupmax  11508  minmax  11512  2zinfmin  11525  xrmaxleim  11526  xrmaxiflemlub  11530  xrmaxiflemcom  11531  xrmaxiflemval  11532  xrmaxleastlt  11538  xrmaxltsup  11540  xrmaxaddlem  11542  xrmaxadd  11543  xrminmax  11547  xrmin1inf  11549  xrmin2inf  11550  xrmineqinf  11551  climi  11569  reccn2ap  11595  climge0  11607  climle  11616  climserle  11627  climrecvg1n  11630  fz1f1o  11657  summodclem3  11662  summodclem2a  11663  summodc  11665  fisumss  11674  fsum0diaglem  11722  mptfzshft  11724  fsumrev  11725  fisum0diag2  11729  fsumlessfi  11742  fsumle  11745  fsumlt  11746  isumsplit  11773  isumrpcl  11776  expcnvap0  11784  geosergap  11788  pwm1geoserap1  11790  absgtap  11792  geolim  11793  geolim2  11794  georeclim  11795  geoisumr  11800  geoisum1c  11802  cvgratnnlembern  11805  cvgratnnlemseq  11808  cvgratnnlemsumlt  11810  cvgratnnlemfm  11811  cvgratnnlemrate  11812  cvgratnn  11813  cvgratz  11814  mertenslemub  11816  mertenslemi1  11817  mertenslem2  11818  mertensabs  11819  prodmodclem2a  11858  prodmodc  11860  zproddc  11861  fprodntrivap  11866  fprodf1o  11870  fprodssdc  11872  fprodsplitdc  11878  fprodrev  11901  fprodmodd  11923  efcllemp  11940  ege2le3  11953  eftlcvg  11969  eftlub  11972  efltim  11980  eflegeo  11983  tanaddap  12021  sinbnd  12034  cosbnd  12035  sin01bnd  12039  cos01bnd  12040  sinltxirr  12043  sin01gt0  12044  cos01gt0  12045  cos12dec  12050  eirraplem  12059  zdvdsdc  12094  dvdstr  12110  dvdsadd2b  12122  fsumdvds  12124  dvdslelemd  12125  divconjdvds  12131  alzdvds  12136  dvdsext  12137  fzm1ndvds  12138  fzo0dvdseq  12139  3dvds  12146  zeo3  12150  even2n  12156  mod2eq1n2dvds  12161  nn0ehalf  12185  nnehalf  12186  nno  12188  nn0oddm1d2  12191  divalglemnqt  12202  divalglemex  12204  divalglemeuneg  12205  divalg2  12208  divalgmod  12209  flodddiv4t2lthalf  12221  bitsfzolem  12236  bitsfzo  12237  bitsmod  12238  bitsfi  12239  bitscmp  12240  bitsinv1lem  12243  bitsinv1  12244  dvdsbnd  12248  gcdsupex  12249  gcdsupcl  12250  gcddvds  12255  divgcdz  12263  divgcdnn  12267  gcd0id  12271  gcdneg  12274  gcd1  12279  dvdsgcdidd  12286  bezoutlemnewy  12288  bezoutlemstep  12289  bezoutlemmo  12298  bezoutlemsup  12301  dfgcd3  12302  bezout  12303  dfgcd2  12306  mulgcd  12308  sqgcd  12321  dvdssqlem  12322  bezoutr1  12325  uzwodc  12329  nninfctlemfo  12332  lcmval  12356  lcmcllem  12360  dvdslcm  12362  lcmgcdlem  12370  lcmdvds  12372  lcmgcdeq  12376  ncoprmgcdne1b  12382  mulgcddvds  12387  rpmulgcd2  12388  qredeu  12390  rpdvds  12392  prmind2  12413  nprm  12416  dvdsnprmd  12418  isprm5lem  12434  isprm5  12435  divgcdodd  12436  isprm6  12440  prmexpb  12444  pw2dvds  12459  pw2dvdseulemle  12460  oddpwdclemdc  12466  sqne2sq  12470  znege1  12471  sqrt2irraplemnn  12472  divnumden  12489  divdenle  12490  qden1elz  12498  nn0sqrtelqelz  12499  hashdvds  12514  crth  12517  phimullem  12518  eulerthlemfi  12521  eulerthlemh  12524  eulerthlemth  12525  eulerth  12526  prmdiv  12528  prmdiveq  12529  hashgcdlem  12531  dvdsfi  12532  phisum  12534  odzcllem  12536  odzdvds  12539  odzphi  12540  oddprm  12553  pythagtriplem3  12561  pythagtriplem4  12562  pythagtriplem10  12563  pythagtriplem11  12568  pythagtriplem13  12570  pythagtriplem19  12576  pcprendvds  12584  pcprendvds2  12585  pcpre1  12586  pcpremul  12587  pceulem  12588  pceu  12589  pczpre  12591  pcmul  12595  pcdiv  12596  pcqmul  12597  pcqdiv  12601  pcexp  12603  pcidlem  12617  pcneg  12619  pcdvdstr  12621  pcgcd1  12622  pc2dvds  12624  dvdsprmpweq  12629  dvdsprmpweqle  12631  pcaddlem  12633  pcadd  12634  pcadd2  12635  pcmpt  12637  fldivp1  12642  pcfaclem  12643  pcfac  12644  pcbc  12645  qexpz  12646  oddprmdvds  12648  pockthlem  12650  pockthg  12651  infpnlem2  12654  1arith  12661  4sqlem9  12680  4sqlem10  12681  4sqlem11  12695  4sqlem12  12696  4sqlem13m  12697  4sqlem14  12698  4sqlem16  12700  oddennn  12734  ennnfonelemk  12742  ennnfonelemkh  12754  ennnfonelemhf1o  12755  ennnfonelemex  12756  ennnfonelemhom  12757  ennnfonelemrnh  12758  ennnfonelemen  12763  ennnfonelemim  12766  ctinfomlemom  12769  ctiunctlemf  12780  ssnnctlemct  12788  nninfdclemcl  12790  nninfdclemp1  12792  nninfdclemlt  12793  unbendc  12796  prdsbascl  13092  pwselbas  13097  mgmb1mgm1  13171  mgm1  13173  mgmidsssn0  13187  gsumfzval  13194  gsumress  13198  gsum0g  13199  gsumval2  13200  sgrp1  13214  sgrpidmndm  13223  ismndd  13240  prds0g  13252  mhmpropd  13269  resmhm  13290  resmhm2b  13292  gsumwsubmcl  13299  gsumwmhm  13301  isgrpd2e  13323  grpidd2  13344  isgrpinv  13357  grpinvinv  13370  grpidssd  13379  grpinvssd  13380  mulgval  13429  mulgfng  13431  mulgnegnn  13439  subg0  13487  issubg4m  13500  nsgconj  13513  1nsgtrivd  13526  eqgen  13534  eqgcpbl  13535  qus0  13542  ghmid  13556  resghm  13567  ghmnsgpreima  13576  kerf1ghm  13581  conjsubgen  13585  conjnmz  13586  imasabl  13643  rnglz  13678  rngrz  13679  qusrng  13691  issrgid  13714  srg1zr  13720  ringcl  13746  isringid  13758  ringcom  13764  ringpropd  13771  ringlz  13776  ringrz  13777  ring1  13792  opprrng  13810  opprring  13812  dvdsrcld  13830  unitcld  13841  unitmulcl  13846  unitgrp  13849  unitnegcl  13863  rhmmul  13897  isrhm2d  13898  rhmdvdsr  13908  rhmopp  13909  elrhmunit  13910  rhmunitinv  13911  subrgugrp  13973  aprsym  14017  islmodd  14026  lmod0vs  14054  lmodfopne  14059  lmodcom  14066  lssclg  14097  lspsnel5a  14143  lspsneq0b  14160  lsslsp  14162  sraring  14182  sralmod  14183  rspssp  14227  rnglidlmsgrp  14230  2idlcpblrng  14256  gsumfzfsumlem0  14319  zncrng  14378  znzrh2  14379  znzrhfo  14381  znf1o  14384  znfi  14388  znhash  14389  znidom  14390  znidomb  14391  znunit  14392  znrrg  14393  psrbaglesuppg  14405  psrelbas  14408  psrelbasfi  14409  psrgrp  14418  psr0  14419  psr1clfi  14421  mplsubgfilemcl  14432  mplsubgfileminv  14433  ntridm  14569  ntrtop  14571  ntrcls0  14574  ntr0  14577  isopn3i  14578  neiss2  14585  opnneiss  14601  topssnei  14605  cnpf2  14650  icnpimaex  14654  lmcvg  14660  iscnp4  14661  cncnp  14673  cnptopresti  14681  lmfss  14687  lmtopcnp  14693  hmeores  14758  bldisj  14844  xblss2ps  14847  xblss2  14848  blhalf  14851  blssps  14870  blss  14871  ssblex  14874  blpnfctr  14882  xmetresbl  14883  mopni2  14926  bdxmet  14944  bdbl  14946  xmetxpbl  14951  metcnpi  14958  metcnpi2  14959  tgioo  14997  rescncf  15024  mulcncflem  15050  cnopnap  15054  dedekindeulemuub  15060  dedekindeulemloc  15062  dedekindeulemlu  15064  dedekindeu  15066  dedekindicclemuub  15069  dedekindicclemloc  15071  dedekindicclemlu  15073  dedekindicclemicc  15075  dedekindicc  15076  ivthinclemlopn  15079  ivthinclemuopn  15081  ivthdec  15087  ivthreinc  15088  hovergt0  15093  dich0  15095  limcimolemlt  15107  cnplimcim  15110  cnplimclemr  15112  limccnpcntop  15118  limccnp2cntop  15120  limccoap  15121  dvfgg  15131  dvidlemap  15134  dvidrelem  15135  dvidsslem  15136  dvaddxxbr  15144  dvmulxxbr  15145  dvaddxx  15146  dvmulxx  15147  dviaddf  15148  dvimulf  15149  dvcoapbr  15150  dvcjbr  15151  dvcj  15152  dvrecap  15156  dvmptclx  15161  dveflem  15169  elply2  15178  plyf  15180  plyaddlem  15192  plymullem  15193  plycoeid3  15200  plyco  15202  plycj  15204  dvply1  15208  dvply2g  15209  reeff1oleme  15215  eflt  15218  sin0pilem1  15224  pilem3  15226  cosq14gt0  15275  coseq0negpitopi  15279  tangtx  15281  coskpi  15291  cosordlem  15292  cosq34lt1  15293  relogef  15307  logrpap0d  15321  rplogcl  15322  logge0  15323  logdivlti  15324  cxplt3  15363  rpabscxpbnd  15383  dvdsppwf1o  15432  fsumdvdsmul  15434  mersenne  15440  perfect1  15441  perfectlem1  15442  perfectlem2  15443  perfect  15444  lgslem1  15448  lgsval  15452  lgsfvalg  15453  lgsval2lem  15458  lgsvalmod  15467  lgsfcl3  15469  lgsmod  15474  lgsdirprm  15482  lgsdir  15483  lgsdilem2  15484  lgsdi  15485  lgsne0  15486  gausslemma2dlem0i  15505  gausslemma2dlem1a  15506  gausslemma2dlem1f1o  15508  gausslemma2dlem3  15511  gausslemma2dlem4  15512  lgseisenlem1  15518  lgseisenlem2  15519  lgseisenlem3  15520  lgseisenlem4  15521  lgseisen  15522  lgsquadlem1  15525  lgsquadlem2  15526  lgsquadlem3  15527  lgsquad2lem1  15529  lgsquad2lem2  15530  lgsquad3  15532  2lgslem1c  15538  2lgsoddprm  15561  2sqlem3  15565  2sqlem4  15566  2sqlem8  15571  bj-charfunr  15708  2omap  15894  pwf1oexmid  15898  subctctexmid  15899  domomsubct  15900  pw1nct  15902  nnsf  15904  peano4nninf  15905  nninfsellemeq  15913  nnnninfex  15921  cvgcmp2nlemabs  15933  iooref1o  15935  trilpolemisumle  15939  trilpolemeq1  15941  trilpolemlt1  15942  trirec0  15945  apdifflemf  15947  apdifflemr  15948  apdiff  15949  iswomninnlem  15950  redcwlpo  15956  redc0  15958  reap0  15959  nconstwlpolemgt0  15965  neapmkvlem  15968  ltlenmkv  15971  supfz  15972  inffz  15973