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  1853  eqtrd  2238  eleqtrd  2284  neeqtrd  2404  3netr3d  2408  rexlimd2  2621  raleqtrdv  2710  rexeqtrdv  2711  ceqsalt  2798  vtoclgft  2823  vtoclegft  2845  elrab3t  2928  eueq2dc  2946  sbceq1dd  3004  csbiedf  3134  sseqtrd  3231  3sstr3d  3237  ifbothdadc  3604  snssd  3778  dfnfc2  3868  breqdi  4059  breqtrd  4070  3brtr3d  4075  csbexga  4172  reuhypd  4518  reg2exmidlema  4582  elirr  4589  en2lp  4602  onsucuni2  4612  finds  4648  iota4  5251  iota4an  5252  funimaexglem  5357  fneu  5380  fco2  5442  fssres2  5453  fresin  5454  feu  5458  f1orescnv  5538  resdif  5544  funcocnv2  5547  f1oprg  5566  fvelrnb  5626  fimacnv  5709  f1oresrab  5745  fsn2  5754  xpsng  5755  funopsn  5762  fnressn  5770  fsnunf  5784  foeqcnvco  5859  isores1  5883  isoini2  5888  riota5f  5924  riotass2  5926  riotass  5927  ovmpodxf  6071  uchoice  6223  elopabi  6281  cnvf1o  6311  smores3  6379  tfrlemisucaccv  6411  tfr1onlemsucaccv  6427  tfrcllemsucaccv  6440  rdgon  6472  frecabcl  6485  frecsuclem  6492  nnsucsssuc  6578  nnsucuniel  6581  erref  6640  iserd  6646  swoer  6648  swoord1  6649  swoord2  6650  erth  6666  erthi  6668  eroveu  6713  pmresg  6763  mapsn  6777  fndmeng  6902  xpen  6942  phplem4  6952  phplem4on  6964  fidifsnen  6967  dif1en  6976  dif1enen  6977  fisbth  6980  diffisn  6990  ac6sfi  6995  fimax2gtri  6998  en2eqpr  7004  unsnfidcex  7017  unsnfidcel  7018  prfidceq  7025  fiintim  7028  fidcenumlemrks  7055  elfi2  7074  elfir  7075  fiuni  7080  fifo  7082  eqsupti  7098  supisoti  7112  ordiso2  7137  casef  7190  difinfsnlem  7201  ctmlemr  7210  ctssdccl  7213  enumct  7217  nninfninc  7225  nnnninfeq  7230  nnnninfeq2  7231  enomnilem  7240  exmidomni  7244  fodjum  7248  fodjuomnilemres  7250  mkvprop  7260  enmkvlem  7263  enwomnilem  7271  nninfdcinf  7273  nninfwlpoimlemdc  7279  nninfinfwlpolem  7280  acfun  7319  2omotaplemap  7369  exmidmotap  7373  ccfunen  7376  cc2lem  7378  dfplpq2  7467  ltanqi  7515  ltmnqi  7516  ltaddnq  7520  subhalfnqq  7527  ltbtwnnqq  7528  archnqq  7530  prarloclemarch2  7532  enq0sym  7545  enq0ref  7546  enq0tr  7547  nqnq0pi  7551  nnnq0lem1  7559  distrnq0  7572  prarloclemlt  7606  prarloclemn  7612  prarloclemcalc  7615  genplt2i  7623  addnqprllem  7640  addnqprulem  7641  addlocprlemgt  7647  appdivnq  7676  prmuloc2  7680  ltexprlemopl  7714  ltexprlemopu  7716  ltexprlemru  7725  prplnqu  7733  cauappcvgprlemopl  7759  cauappcvgprlemlol  7760  cauappcvgprlemladdfu  7767  cauappcvgprlemladdrl  7770  cauappcvgprlem1  7772  archrecnq  7776  archrecpr  7777  caucvgprlemk  7778  caucvgprlemnbj  7780  caucvgprlemm  7781  caucvgprlemopl  7782  caucvgprlemlol  7783  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  caucvgprlem1  7792  caucvgprprlemk  7796  caucvgprprlemnkeqj  7803  caucvgprprlemnbj  7806  caucvgprprlemml  7807  caucvgprprlemmu  7808  caucvgprprlemopl  7810  caucvgprprlemlol  7811  caucvgprprlemopu  7812  caucvgprprlemexbt  7819  caucvgprprlemexb  7820  caucvgprprlem1  7822  caucvgprprlem2  7823  suplocexprlemru  7832  suplocexprlemdisj  7833  suplocexprlemloc  7834  suplocexprlemub  7836  suplocexprlemlub  7837  prsrlem1  7855  addgt0sr  7888  srpospr  7896  prsrriota  7901  caucvgsrlemgt1  7908  caucvgsrlemoffgt1  7912  caucvgsr  7915  mappsrprg  7917  suplocsrlemb  7919  suplocsrlempr  7920  suplocsrlem  7921  recriota  8003  axsuploc  8145  lelttr  8161  ltletr  8162  ltnsymd  8192  lensymd  8194  cnegexlem3  8249  cnegex2  8251  addcanad  8258  addcan2ad  8259  negcon1ad  8378  negne0d  8381  negrebd  8382  subeq0d  8391  subne0ad  8394  neg11d  8395  subcand  8424  subcan2d  8425  ltadd2  8492  ltadd2dd  8495  add20  8547  ltnegcon1d  8598  ltnegcon2d  8599  lenegcon1d  8600  lenegcon2d  8601  subled  8621  lesubd  8622  ltsub23d  8623  ltsub13d  8624  ltadd1dd  8629  ltsub1dd  8630  ltsub2dd  8631  leadd1dd  8632  leadd2dd  8633  lesub1dd  8634  lesub2dd  8635  recexre  8651  apreap  8660  ltmul1a  8664  reapmul1  8668  cru  8675  apreim  8676  mulge0  8692  leltap  8698  negap0d  8704  ltleap  8705  ltapd  8711  ap0gt0  8713  ap0gt0d  8714  mulcanapad  8736  mulcanap2ad  8737  eqnegad  8807  diveqap0d  8870  diveqap1d  8871  divap1d  8874  rec11apd  8884  div11apd  8904  div2subap  8910  recgt0  8923  prodgt0  8925  lemul1a  8931  lemulge12  8940  lt2msq1  8958  lediv12a  8967  recreclt  8973  nn1suc  9055  nnnlt1  9062  nn2ge  9069  nn1gt1  9070  nnrecl  9293  nn0nlt0  9321  elnn0z  9385  nnnle0  9421  nn0negleid  9441  elz2  9444  nn0n0n1ge2b  9452  nnm1ge0  9459  nn0ge0div  9460  zextle  9464  suprzclex  9471  nn0ind-raph  9490  zindd  9491  uzneg  9667  eluzadd  9677  eluzsub  9678  uzm1  9679  uz3m2nn  9694  supminfex  9718  infregelbex  9719  nn01to3  9738  irrmulap  9769  ltrec1d  9839  lerec2d  9840  ledivdivd  9844  divge1  9845  ltmul1dd  9874  ltmul2dd  9875  ltdiv1dd  9876  lediv1dd  9877  ltdiv23d  9879  lediv23d  9880  nn0ledivnn  9889  addlelt  9890  xrlelttr  9928  xrltletr  9929  xaddass2  9992  xltadd1  9998  xlt2add  10002  ixxdisj  10025  icoshftf1o  10113  icodisj  10114  lincmb01cmp  10125  iccf1o  10126  uzsubsubfz  10169  fzdisj  10174  fzopth  10183  fznatpl1  10198  fzsuc2  10201  fzp1disj  10202  fzrev2i  10208  uzdisj  10215  fseq1p1m1  10216  fzm1  10222  fzneuz  10223  fzp1nel  10226  fzrevral  10227  fznn0sub2  10250  fz0fzdiffz0  10252  difelfzle  10256  difelfznle  10257  nn0disj  10260  fzonnsub  10293  fzodisj  10302  fzouzdisj  10304  eluzgtdifelfzo  10326  ubmelfzo  10329  fzonn0p1p1  10342  ubmelm1fzo  10355  fzostep1  10366  exfzdc  10369  subfzo0  10371  zsupcllemstep  10372  infssuzex  10376  zsupssdc  10381  qtri3or  10383  exbtwnzlemex  10392  rebtwn2z  10397  qbtwnrelemcalc  10398  qbtwnre  10399  qavgle  10401  apbtwnz  10417  flid  10427  flqwordi  10431  flqmulnn0  10442  flhalf  10445  flltdivnn0lt  10447  fldiv4p1lem1div2  10448  intfracq  10465  flqdiv  10466  flqpmodeq  10472  modqmulnn  10487  mulqaddmodid  10509  modqmuladdim  10512  modqmuladdnn0  10513  m1modge3gt1  10516  q2submod  10530  modaddmodup  10532  modqsubdir  10538  modqeqmodmin  10539  modfzo0difsn  10540  uzennn  10581  uzsinds  10589  monoord2  10631  ser3mono  10632  iseqf1olemqcl  10644  iseqf1olemnab  10646  iseqf1olemab  10647  iseqf1olemqf1o  10651  iseqf1olemqk  10652  seq3f1olemqsumkj  10656  seq3f1olemqsumk  10657  seq3f1olemqsum  10658  seq3f1olemp  10660  seqf1oglem1  10664  seqf1oglem2  10665  ser3le  10682  exp3val  10686  expnegap0  10692  expgt1  10722  ltexp2a  10736  le2sq2  10760  nnlesq  10788  qsqeqor  10795  bernneq  10805  expnbnd  10808  expnlbnd  10809  expnlbnd2  10810  expeq0d  10814  sq11d  10851  nn0ltexp2  10854  expcand  10862  nn0opthd  10867  facdiv  10883  faclbnd6  10889  facubnd  10890  facavg  10891  bcval4  10897  bcp1nk  10907  bcval5  10908  bcpasc  10911  hashennnuni  10924  isfinite4im  10937  hashnncl  10940  hashunlem  10949  fiprsshashgt1  10962  hashfzp1  10969  zfz1isolemiso  10984  seq3coll  10987  hash2en  10988  iswrdiz  11001  wrdffz  11015  ccatval21sw  11061  ccatass  11064  swrdf  11108  swrdlend  11111  ccatswrd  11123  swrdccat2  11124  seq3shft  11149  cjth  11157  cjdivap  11220  cjne0d  11258  cjap0d  11259  cvg1nlemcxze  11293  cvg1nlemcau  11295  cvg1nlemres  11296  recvguniq  11306  resqrexlemover  11321  resqrexlemdecn  11323  resqrexlemlo  11324  resqrexlemcalc2  11326  resqrexlemcalc3  11327  resqrexlemnmsq  11328  resqrexlemnm  11329  resqrexlemcvg  11330  resqrexlemglsq  11333  resqrexlemga  11334  leabs  11385  absrele  11394  nn0abscl  11396  ltabs  11398  abslt  11399  absle  11400  abstri  11415  amgm2  11429  sqr11d  11484  abs00d  11497  maxabsle  11515  maxabslemlub  11518  maxleastlt  11526  maxltsup  11529  2zsupmax  11537  minmax  11541  2zinfmin  11554  xrmaxleim  11555  xrmaxiflemlub  11559  xrmaxiflemcom  11560  xrmaxiflemval  11561  xrmaxleastlt  11567  xrmaxltsup  11569  xrmaxaddlem  11571  xrmaxadd  11572  xrminmax  11576  xrmin1inf  11578  xrmin2inf  11579  xrmineqinf  11580  climi  11598  reccn2ap  11624  climge0  11636  climle  11645  climserle  11656  climrecvg1n  11659  fz1f1o  11686  summodclem3  11691  summodclem2a  11692  summodc  11694  fisumss  11703  fsum0diaglem  11751  mptfzshft  11753  fsumrev  11754  fisum0diag2  11758  fsumlessfi  11771  fsumle  11774  fsumlt  11775  isumsplit  11802  isumrpcl  11805  expcnvap0  11813  geosergap  11817  pwm1geoserap1  11819  absgtap  11821  geolim  11822  geolim2  11823  georeclim  11824  geoisumr  11829  geoisum1c  11831  cvgratnnlembern  11834  cvgratnnlemseq  11837  cvgratnnlemsumlt  11839  cvgratnnlemfm  11840  cvgratnnlemrate  11841  cvgratnn  11842  cvgratz  11843  mertenslemub  11845  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  prodmodclem2a  11887  prodmodc  11889  zproddc  11890  fprodntrivap  11895  fprodf1o  11899  fprodssdc  11901  fprodsplitdc  11907  fprodrev  11930  fprodmodd  11952  efcllemp  11969  ege2le3  11982  eftlcvg  11998  eftlub  12001  efltim  12009  eflegeo  12012  tanaddap  12050  sinbnd  12063  cosbnd  12064  sin01bnd  12068  cos01bnd  12069  sinltxirr  12072  sin01gt0  12073  cos01gt0  12074  cos12dec  12079  eirraplem  12088  zdvdsdc  12123  dvdstr  12139  dvdsadd2b  12151  fsumdvds  12153  dvdslelemd  12154  divconjdvds  12160  alzdvds  12165  dvdsext  12166  fzm1ndvds  12167  fzo0dvdseq  12168  3dvds  12175  zeo3  12179  even2n  12185  mod2eq1n2dvds  12190  nn0ehalf  12214  nnehalf  12215  nno  12217  nn0oddm1d2  12220  divalglemnqt  12231  divalglemex  12233  divalglemeuneg  12234  divalg2  12237  divalgmod  12238  flodddiv4t2lthalf  12250  bitsfzolem  12265  bitsfzo  12266  bitsmod  12267  bitsfi  12268  bitscmp  12269  bitsinv1lem  12272  bitsinv1  12273  dvdsbnd  12277  gcdsupex  12278  gcdsupcl  12279  gcddvds  12284  divgcdz  12292  divgcdnn  12296  gcd0id  12300  gcdneg  12303  gcd1  12308  dvdsgcdidd  12315  bezoutlemnewy  12317  bezoutlemstep  12318  bezoutlemmo  12327  bezoutlemsup  12330  dfgcd3  12331  bezout  12332  dfgcd2  12335  mulgcd  12337  sqgcd  12350  dvdssqlem  12351  bezoutr1  12354  uzwodc  12358  nninfctlemfo  12361  lcmval  12385  lcmcllem  12389  dvdslcm  12391  lcmgcdlem  12399  lcmdvds  12401  lcmgcdeq  12405  ncoprmgcdne1b  12411  mulgcddvds  12416  rpmulgcd2  12417  qredeu  12419  rpdvds  12421  prmind2  12442  nprm  12445  dvdsnprmd  12447  isprm5lem  12463  isprm5  12464  divgcdodd  12465  isprm6  12469  prmexpb  12473  pw2dvds  12488  pw2dvdseulemle  12489  oddpwdclemdc  12495  sqne2sq  12499  znege1  12500  sqrt2irraplemnn  12501  divnumden  12518  divdenle  12519  qden1elz  12527  nn0sqrtelqelz  12528  hashdvds  12543  crth  12546  phimullem  12547  eulerthlemfi  12550  eulerthlemh  12553  eulerthlemth  12554  eulerth  12555  prmdiv  12557  prmdiveq  12558  hashgcdlem  12560  dvdsfi  12561  phisum  12563  odzcllem  12565  odzdvds  12568  odzphi  12569  oddprm  12582  pythagtriplem3  12590  pythagtriplem4  12591  pythagtriplem10  12592  pythagtriplem11  12597  pythagtriplem13  12599  pythagtriplem19  12605  pcprendvds  12613  pcprendvds2  12614  pcpre1  12615  pcpremul  12616  pceulem  12617  pceu  12618  pczpre  12620  pcmul  12624  pcdiv  12625  pcqmul  12626  pcqdiv  12630  pcexp  12632  pcidlem  12646  pcneg  12648  pcdvdstr  12650  pcgcd1  12651  pc2dvds  12653  dvdsprmpweq  12658  dvdsprmpweqle  12660  pcaddlem  12662  pcadd  12663  pcadd2  12664  pcmpt  12666  fldivp1  12671  pcfaclem  12672  pcfac  12673  pcbc  12674  qexpz  12675  oddprmdvds  12677  pockthlem  12679  pockthg  12680  infpnlem2  12683  1arith  12690  4sqlem9  12709  4sqlem10  12710  4sqlem11  12724  4sqlem12  12725  4sqlem13m  12726  4sqlem14  12727  4sqlem16  12729  oddennn  12763  ennnfonelemk  12771  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ennnfonelemex  12785  ennnfonelemhom  12786  ennnfonelemrnh  12787  ennnfonelemen  12792  ennnfonelemim  12795  ctinfomlemom  12798  ctiunctlemf  12809  ssnnctlemct  12817  nninfdclemcl  12819  nninfdclemp1  12821  nninfdclemlt  12822  unbendc  12825  prdsbascl  13121  pwselbas  13126  mgmb1mgm1  13200  mgm1  13202  mgmidsssn0  13216  gsumfzval  13223  gsumress  13227  gsum0g  13228  gsumval2  13229  sgrp1  13243  sgrpidmndm  13252  ismndd  13269  prds0g  13281  mhmpropd  13298  resmhm  13319  resmhm2b  13321  gsumwsubmcl  13328  gsumwmhm  13330  isgrpd2e  13352  grpidd2  13373  isgrpinv  13386  grpinvinv  13399  grpidssd  13408  grpinvssd  13409  mulgval  13458  mulgfng  13460  mulgnegnn  13468  subg0  13516  issubg4m  13529  nsgconj  13542  1nsgtrivd  13555  eqgen  13563  eqgcpbl  13564  qus0  13571  ghmid  13585  resghm  13596  ghmnsgpreima  13605  kerf1ghm  13610  conjsubgen  13614  conjnmz  13615  imasabl  13672  rnglz  13707  rngrz  13708  qusrng  13720  issrgid  13743  srg1zr  13749  ringcl  13775  isringid  13787  ringcom  13793  ringpropd  13800  ringlz  13805  ringrz  13806  ring1  13821  opprrng  13839  opprring  13841  dvdsrcld  13859  unitcld  13870  unitmulcl  13875  unitgrp  13878  unitnegcl  13892  rhmmul  13926  isrhm2d  13927  rhmdvdsr  13937  rhmopp  13938  elrhmunit  13939  rhmunitinv  13940  subrgugrp  14002  aprsym  14046  islmodd  14055  lmod0vs  14083  lmodfopne  14088  lmodcom  14095  lssclg  14126  lspsnel5a  14172  lspsneq0b  14189  lsslsp  14191  sraring  14211  sralmod  14212  rspssp  14256  rnglidlmsgrp  14259  2idlcpblrng  14285  gsumfzfsumlem0  14348  zncrng  14407  znzrh2  14408  znzrhfo  14410  znf1o  14413  znfi  14417  znhash  14418  znidom  14419  znidomb  14420  znunit  14421  znrrg  14422  psrbaglesuppg  14434  psrelbas  14437  psrelbasfi  14438  psrgrp  14447  psr0  14448  psr1clfi  14450  mplsubgfilemcl  14461  mplsubgfileminv  14462  ntridm  14598  ntrtop  14600  ntrcls0  14603  ntr0  14606  isopn3i  14607  neiss2  14614  opnneiss  14630  topssnei  14634  cnpf2  14679  icnpimaex  14683  lmcvg  14689  iscnp4  14690  cncnp  14702  cnptopresti  14710  lmfss  14716  lmtopcnp  14722  hmeores  14787  bldisj  14873  xblss2ps  14876  xblss2  14877  blhalf  14880  blssps  14899  blss  14900  ssblex  14903  blpnfctr  14911  xmetresbl  14912  mopni2  14955  bdxmet  14973  bdbl  14975  xmetxpbl  14980  metcnpi  14987  metcnpi2  14988  tgioo  15026  rescncf  15053  mulcncflem  15079  cnopnap  15083  dedekindeulemuub  15089  dedekindeulemloc  15091  dedekindeulemlu  15093  dedekindeu  15095  dedekindicclemuub  15098  dedekindicclemloc  15100  dedekindicclemlu  15102  dedekindicclemicc  15104  dedekindicc  15105  ivthinclemlopn  15108  ivthinclemuopn  15110  ivthdec  15116  ivthreinc  15117  hovergt0  15122  dich0  15124  limcimolemlt  15136  cnplimcim  15139  cnplimclemr  15141  limccnpcntop  15147  limccnp2cntop  15149  limccoap  15150  dvfgg  15160  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvaddxxbr  15173  dvmulxxbr  15174  dvaddxx  15175  dvmulxx  15176  dviaddf  15177  dvimulf  15178  dvcoapbr  15179  dvcjbr  15180  dvcj  15181  dvrecap  15185  dvmptclx  15190  dveflem  15198  elply2  15207  plyf  15209  plyaddlem  15221  plymullem  15222  plycoeid3  15229  plyco  15231  plycj  15233  dvply1  15237  dvply2g  15238  reeff1oleme  15244  eflt  15247  sin0pilem1  15253  pilem3  15255  cosq14gt0  15304  coseq0negpitopi  15308  tangtx  15310  coskpi  15320  cosordlem  15321  cosq34lt1  15322  relogef  15336  logrpap0d  15350  rplogcl  15351  logge0  15352  logdivlti  15353  cxplt3  15392  rpabscxpbnd  15412  dvdsppwf1o  15461  fsumdvdsmul  15463  mersenne  15469  perfect1  15470  perfectlem1  15471  perfectlem2  15472  perfect  15473  lgslem1  15477  lgsval  15481  lgsfvalg  15482  lgsval2lem  15487  lgsvalmod  15496  lgsfcl3  15498  lgsmod  15503  lgsdirprm  15511  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  gausslemma2dlem0i  15534  gausslemma2dlem1a  15535  gausslemma2dlem1f1o  15537  gausslemma2dlem3  15540  gausslemma2dlem4  15541  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgseisenlem4  15550  lgseisen  15551  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad2lem1  15558  lgsquad2lem2  15559  lgsquad3  15561  2lgslem1c  15567  2lgsoddprm  15590  2sqlem3  15594  2sqlem4  15595  2sqlem8  15600  bj-charfunr  15746  2omap  15932  pwf1oexmid  15936  subctctexmid  15937  domomsubct  15938  pw1nct  15940  nnsf  15942  peano4nninf  15943  nninfsellemeq  15951  nnnninfex  15959  cvgcmp2nlemabs  15971  iooref1o  15973  trilpolemisumle  15977  trilpolemeq1  15979  trilpolemlt1  15980  trirec0  15983  apdifflemf  15985  apdifflemr  15986  apdiff  15987  iswomninnlem  15988  redcwlpo  15994  redc0  15996  reap0  15997  nconstwlpolemgt0  16003  neapmkvlem  16006  ltlenmkv  16009  supfz  16010  inffz  16011