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  11091  cjth  11099  cjdivap  11162  cjne0d  11200  cjap0d  11201  cvg1nlemcxze  11235  cvg1nlemcau  11237  cvg1nlemres  11238  recvguniq  11248  resqrexlemover  11263  resqrexlemdecn  11265  resqrexlemlo  11266  resqrexlemcalc2  11268  resqrexlemcalc3  11269  resqrexlemnmsq  11270  resqrexlemnm  11271  resqrexlemcvg  11272  resqrexlemglsq  11275  resqrexlemga  11276  leabs  11327  absrele  11336  nn0abscl  11338  ltabs  11340  abslt  11341  absle  11342  abstri  11357  amgm2  11371  sqr11d  11426  abs00d  11439  maxabsle  11457  maxabslemlub  11460  maxleastlt  11468  maxltsup  11471  2zsupmax  11479  minmax  11483  2zinfmin  11496  xrmaxleim  11497  xrmaxiflemlub  11501  xrmaxiflemcom  11502  xrmaxiflemval  11503  xrmaxleastlt  11509  xrmaxltsup  11511  xrmaxaddlem  11513  xrmaxadd  11514  xrminmax  11518  xrmin1inf  11520  xrmin2inf  11521  xrmineqinf  11522  climi  11540  reccn2ap  11566  climge0  11578  climle  11587  climserle  11598  climrecvg1n  11601  fz1f1o  11628  summodclem3  11633  summodclem2a  11634  summodc  11636  fisumss  11645  fsum0diaglem  11693  mptfzshft  11695  fsumrev  11696  fisum0diag2  11700  fsumlessfi  11713  fsumle  11716  fsumlt  11717  isumsplit  11744  isumrpcl  11747  expcnvap0  11755  geosergap  11759  pwm1geoserap1  11761  absgtap  11763  geolim  11764  geolim2  11765  georeclim  11766  geoisumr  11771  geoisum1c  11773  cvgratnnlembern  11776  cvgratnnlemseq  11779  cvgratnnlemsumlt  11781  cvgratnnlemfm  11782  cvgratnnlemrate  11783  cvgratnn  11784  cvgratz  11785  mertenslemub  11787  mertenslemi1  11788  mertenslem2  11789  mertensabs  11790  prodmodclem2a  11829  prodmodc  11831  zproddc  11832  fprodntrivap  11837  fprodf1o  11841  fprodssdc  11843  fprodsplitdc  11849  fprodrev  11872  fprodmodd  11894  efcllemp  11911  ege2le3  11924  eftlcvg  11940  eftlub  11943  efltim  11951  eflegeo  11954  tanaddap  11992  sinbnd  12005  cosbnd  12006  sin01bnd  12010  cos01bnd  12011  sinltxirr  12014  sin01gt0  12015  cos01gt0  12016  cos12dec  12021  eirraplem  12030  zdvdsdc  12065  dvdstr  12081  dvdsadd2b  12093  fsumdvds  12095  dvdslelemd  12096  divconjdvds  12102  alzdvds  12107  dvdsext  12108  fzm1ndvds  12109  fzo0dvdseq  12110  3dvds  12117  zeo3  12121  even2n  12127  mod2eq1n2dvds  12132  nn0ehalf  12156  nnehalf  12157  nno  12159  nn0oddm1d2  12162  divalglemnqt  12173  divalglemex  12175  divalglemeuneg  12176  divalg2  12179  divalgmod  12180  flodddiv4t2lthalf  12192  bitsfzolem  12207  bitsfzo  12208  bitsmod  12209  bitsfi  12210  bitscmp  12211  bitsinv1lem  12214  bitsinv1  12215  dvdsbnd  12219  gcdsupex  12220  gcdsupcl  12221  gcddvds  12226  divgcdz  12234  divgcdnn  12238  gcd0id  12242  gcdneg  12245  gcd1  12250  dvdsgcdidd  12257  bezoutlemnewy  12259  bezoutlemstep  12260  bezoutlemmo  12269  bezoutlemsup  12272  dfgcd3  12273  bezout  12274  dfgcd2  12277  mulgcd  12279  sqgcd  12292  dvdssqlem  12293  bezoutr1  12296  uzwodc  12300  nninfctlemfo  12303  lcmval  12327  lcmcllem  12331  dvdslcm  12333  lcmgcdlem  12341  lcmdvds  12343  lcmgcdeq  12347  ncoprmgcdne1b  12353  mulgcddvds  12358  rpmulgcd2  12359  qredeu  12361  rpdvds  12363  prmind2  12384  nprm  12387  dvdsnprmd  12389  isprm5lem  12405  isprm5  12406  divgcdodd  12407  isprm6  12411  prmexpb  12415  pw2dvds  12430  pw2dvdseulemle  12431  oddpwdclemdc  12437  sqne2sq  12441  znege1  12442  sqrt2irraplemnn  12443  divnumden  12460  divdenle  12461  qden1elz  12469  nn0sqrtelqelz  12470  hashdvds  12485  crth  12488  phimullem  12489  eulerthlemfi  12492  eulerthlemh  12495  eulerthlemth  12496  eulerth  12497  prmdiv  12499  prmdiveq  12500  hashgcdlem  12502  dvdsfi  12503  phisum  12505  odzcllem  12507  odzdvds  12510  odzphi  12511  oddprm  12524  pythagtriplem3  12532  pythagtriplem4  12533  pythagtriplem10  12534  pythagtriplem11  12539  pythagtriplem13  12541  pythagtriplem19  12547  pcprendvds  12555  pcprendvds2  12556  pcpre1  12557  pcpremul  12558  pceulem  12559  pceu  12560  pczpre  12562  pcmul  12566  pcdiv  12567  pcqmul  12568  pcqdiv  12572  pcexp  12574  pcidlem  12588  pcneg  12590  pcdvdstr  12592  pcgcd1  12593  pc2dvds  12595  dvdsprmpweq  12600  dvdsprmpweqle  12602  pcaddlem  12604  pcadd  12605  pcadd2  12606  pcmpt  12608  fldivp1  12613  pcfaclem  12614  pcfac  12615  pcbc  12616  qexpz  12617  oddprmdvds  12619  pockthlem  12621  pockthg  12622  infpnlem2  12625  1arith  12632  4sqlem9  12651  4sqlem10  12652  4sqlem11  12666  4sqlem12  12667  4sqlem13m  12668  4sqlem14  12669  4sqlem16  12671  oddennn  12705  ennnfonelemk  12713  ennnfonelemkh  12725  ennnfonelemhf1o  12726  ennnfonelemex  12727  ennnfonelemhom  12728  ennnfonelemrnh  12729  ennnfonelemen  12734  ennnfonelemim  12737  ctinfomlemom  12740  ctiunctlemf  12751  ssnnctlemct  12759  nninfdclemcl  12761  nninfdclemp1  12763  nninfdclemlt  12764  unbendc  12767  prdsbascl  13063  pwselbas  13068  mgmb1mgm1  13142  mgm1  13144  mgmidsssn0  13158  gsumfzval  13165  gsumress  13169  gsum0g  13170  gsumval2  13171  sgrp1  13185  sgrpidmndm  13194  ismndd  13211  prds0g  13223  mhmpropd  13240  resmhm  13261  resmhm2b  13263  gsumwsubmcl  13270  gsumwmhm  13272  isgrpd2e  13294  grpidd2  13315  isgrpinv  13328  grpinvinv  13341  grpidssd  13350  grpinvssd  13351  mulgval  13400  mulgfng  13402  mulgnegnn  13410  subg0  13458  issubg4m  13471  nsgconj  13484  1nsgtrivd  13497  eqgen  13505  eqgcpbl  13506  qus0  13513  ghmid  13527  resghm  13538  ghmnsgpreima  13547  kerf1ghm  13552  conjsubgen  13556  conjnmz  13557  imasabl  13614  rnglz  13649  rngrz  13650  qusrng  13662  issrgid  13685  srg1zr  13691  ringcl  13717  isringid  13729  ringcom  13735  ringpropd  13742  ringlz  13747  ringrz  13748  ring1  13763  opprrng  13781  opprring  13783  dvdsrcld  13801  unitcld  13812  unitmulcl  13817  unitgrp  13820  unitnegcl  13834  rhmmul  13868  isrhm2d  13869  rhmdvdsr  13879  rhmopp  13880  elrhmunit  13881  rhmunitinv  13882  subrgugrp  13944  aprsym  13988  islmodd  13997  lmod0vs  14025  lmodfopne  14030  lmodcom  14037  lssclg  14068  lspsnel5a  14114  lspsneq0b  14131  lsslsp  14133  sraring  14153  sralmod  14154  rspssp  14198  rnglidlmsgrp  14201  2idlcpblrng  14227  gsumfzfsumlem0  14290  zncrng  14349  znzrh2  14350  znzrhfo  14352  znf1o  14355  znfi  14359  znhash  14360  znidom  14361  znidomb  14362  znunit  14363  znrrg  14364  psrbaglesuppg  14376  psrelbas  14379  psrelbasfi  14380  psrgrp  14389  psr0  14390  psr1clfi  14392  mplsubgfilemcl  14403  mplsubgfileminv  14404  ntridm  14540  ntrtop  14542  ntrcls0  14545  ntr0  14548  isopn3i  14549  neiss2  14556  opnneiss  14572  topssnei  14576  cnpf2  14621  icnpimaex  14625  lmcvg  14631  iscnp4  14632  cncnp  14644  cnptopresti  14652  lmfss  14658  lmtopcnp  14664  hmeores  14729  bldisj  14815  xblss2ps  14818  xblss2  14819  blhalf  14822  blssps  14841  blss  14842  ssblex  14845  blpnfctr  14853  xmetresbl  14854  mopni2  14897  bdxmet  14915  bdbl  14917  xmetxpbl  14922  metcnpi  14929  metcnpi2  14930  tgioo  14968  rescncf  14995  mulcncflem  15021  cnopnap  15025  dedekindeulemuub  15031  dedekindeulemloc  15033  dedekindeulemlu  15035  dedekindeu  15037  dedekindicclemuub  15040  dedekindicclemloc  15042  dedekindicclemlu  15044  dedekindicclemicc  15046  dedekindicc  15047  ivthinclemlopn  15050  ivthinclemuopn  15052  ivthdec  15058  ivthreinc  15059  hovergt0  15064  dich0  15066  limcimolemlt  15078  cnplimcim  15081  cnplimclemr  15083  limccnpcntop  15089  limccnp2cntop  15091  limccoap  15092  dvfgg  15102  dvidlemap  15105  dvidrelem  15106  dvidsslem  15107  dvaddxxbr  15115  dvmulxxbr  15116  dvaddxx  15117  dvmulxx  15118  dviaddf  15119  dvimulf  15120  dvcoapbr  15121  dvcjbr  15122  dvcj  15123  dvrecap  15127  dvmptclx  15132  dveflem  15140  elply2  15149  plyf  15151  plyaddlem  15163  plymullem  15164  plycoeid3  15171  plyco  15173  plycj  15175  dvply1  15179  dvply2g  15180  reeff1oleme  15186  eflt  15189  sin0pilem1  15195  pilem3  15197  cosq14gt0  15246  coseq0negpitopi  15250  tangtx  15252  coskpi  15262  cosordlem  15263  cosq34lt1  15264  relogef  15278  logrpap0d  15292  rplogcl  15293  logge0  15294  logdivlti  15295  cxplt3  15334  rpabscxpbnd  15354  dvdsppwf1o  15403  fsumdvdsmul  15405  mersenne  15411  perfect1  15412  perfectlem1  15413  perfectlem2  15414  perfect  15415  lgslem1  15419  lgsval  15423  lgsfvalg  15424  lgsval2lem  15429  lgsvalmod  15438  lgsfcl3  15440  lgsmod  15445  lgsdirprm  15453  lgsdir  15454  lgsdilem2  15455  lgsdi  15456  lgsne0  15457  gausslemma2dlem0i  15476  gausslemma2dlem1a  15477  gausslemma2dlem1f1o  15479  gausslemma2dlem3  15482  gausslemma2dlem4  15483  lgseisenlem1  15489  lgseisenlem2  15490  lgseisenlem3  15491  lgseisenlem4  15492  lgseisen  15493  lgsquadlem1  15496  lgsquadlem2  15497  lgsquadlem3  15498  lgsquad2lem1  15500  lgsquad2lem2  15501  lgsquad3  15503  2lgslem1c  15509  2lgsoddprm  15532  2sqlem3  15536  2sqlem4  15537  2sqlem8  15542  bj-charfunr  15679  2omap  15865  pwf1oexmid  15869  subctctexmid  15870  domomsubct  15871  pw1nct  15873  nnsf  15875  peano4nninf  15876  nninfsellemeq  15884  nnnninfex  15892  cvgcmp2nlemabs  15904  iooref1o  15906  trilpolemisumle  15910  trilpolemeq1  15912  trilpolemlt1  15913  trirec0  15916  apdifflemf  15918  apdifflemr  15919  apdiff  15920  iswomninnlem  15921  redcwlpo  15927  redc0  15929  reap0  15930  nconstwlpolemgt0  15936  neapmkvlem  15939  ltlenmkv  15942  supfz  15943  inffz  15944