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  1407  equs5or  1841  eqtrd  2226  eleqtrd  2272  neeqtrd  2392  3netr3d  2396  rexlimd2  2609  raleqtrdv  2698  rexeqtrdv  2699  ceqsalt  2786  vtoclgft  2811  vtoclegft  2833  elrab3t  2916  eueq2dc  2934  sbceq1dd  2992  csbiedf  3122  sseqtrd  3218  3sstr3d  3224  ifbothdadc  3590  snssd  3764  dfnfc2  3854  breqdi  4045  breqtrd  4056  3brtr3d  4061  csbexga  4158  reuhypd  4503  reg2exmidlema  4567  elirr  4574  en2lp  4587  onsucuni2  4597  finds  4633  iota4  5235  iota4an  5236  funimaexglem  5338  fneu  5359  fco2  5421  fssres2  5432  fresin  5433  feu  5437  f1orescnv  5517  resdif  5523  funcocnv2  5526  f1oprg  5545  fvelrnb  5605  fimacnv  5688  f1oresrab  5724  fsn2  5733  xpsng  5734  fnressn  5745  fsnunf  5759  foeqcnvco  5834  isores1  5858  isoini2  5863  riota5f  5899  riotass2  5901  riotass  5902  ovmpodxf  6045  uchoice  6192  elopabi  6250  cnvf1o  6280  smores3  6348  tfrlemisucaccv  6380  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  rdgon  6441  frecabcl  6454  frecsuclem  6461  nnsucsssuc  6547  nnsucuniel  6550  erref  6609  iserd  6615  swoer  6617  swoord1  6618  swoord2  6619  erth  6635  erthi  6637  eroveu  6682  pmresg  6732  mapsn  6746  fndmeng  6866  xpen  6903  phplem4  6913  phplem4on  6925  fidifsnen  6928  dif1en  6937  dif1enen  6938  fisbth  6941  diffisn  6951  ac6sfi  6956  fimax2gtri  6959  en2eqpr  6965  unsnfidcex  6978  unsnfidcel  6979  fiintim  6987  fidcenumlemrks  7014  elfi2  7033  elfir  7034  fiuni  7039  fifo  7041  eqsupti  7057  supisoti  7071  ordiso2  7096  casef  7149  difinfsnlem  7160  ctmlemr  7169  ctssdccl  7172  enumct  7176  nninfninc  7184  nnnninfeq  7189  nnnninfeq2  7190  enomnilem  7199  exmidomni  7203  fodjum  7207  fodjuomnilemres  7209  mkvprop  7219  enmkvlem  7222  enwomnilem  7230  nninfdcinf  7232  nninfwlpoimlemdc  7238  acfun  7269  2omotaplemap  7319  exmidmotap  7323  ccfunen  7326  cc2lem  7328  dfplpq2  7416  ltanqi  7464  ltmnqi  7465  ltaddnq  7469  subhalfnqq  7476  ltbtwnnqq  7477  archnqq  7479  prarloclemarch2  7481  enq0sym  7494  enq0ref  7495  enq0tr  7496  nqnq0pi  7500  nnnq0lem1  7508  distrnq0  7521  prarloclemlt  7555  prarloclemn  7561  prarloclemcalc  7564  genplt2i  7572  addnqprllem  7589  addnqprulem  7590  addlocprlemgt  7596  appdivnq  7625  prmuloc2  7629  ltexprlemopl  7663  ltexprlemopu  7665  ltexprlemru  7674  prplnqu  7682  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemladdfu  7716  cauappcvgprlemladdrl  7719  cauappcvgprlem1  7721  archrecnq  7725  archrecpr  7726  caucvgprlemk  7727  caucvgprlemnbj  7729  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprlem1  7741  caucvgprprlemk  7745  caucvgprprlemnkeqj  7752  caucvgprprlemnbj  7755  caucvgprprlemml  7756  caucvgprprlemmu  7757  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemopu  7761  caucvgprprlemexbt  7768  caucvgprprlemexb  7769  caucvgprprlem1  7771  caucvgprprlem2  7772  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemub  7785  suplocexprlemlub  7786  prsrlem1  7804  addgt0sr  7837  srpospr  7845  prsrriota  7850  caucvgsrlemgt1  7857  caucvgsrlemoffgt1  7861  caucvgsr  7864  mappsrprg  7866  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  recriota  7952  axsuploc  8094  lelttr  8110  ltletr  8111  ltnsymd  8141  lensymd  8143  cnegexlem3  8198  cnegex2  8200  addcanad  8207  addcan2ad  8208  negcon1ad  8327  negne0d  8330  negrebd  8331  subeq0d  8340  subne0ad  8343  neg11d  8344  subcand  8373  subcan2d  8374  ltadd2  8440  ltadd2dd  8443  add20  8495  ltnegcon1d  8546  ltnegcon2d  8547  lenegcon1d  8548  lenegcon2d  8549  subled  8569  lesubd  8570  ltsub23d  8571  ltsub13d  8572  ltadd1dd  8577  ltsub1dd  8578  ltsub2dd  8579  leadd1dd  8580  leadd2dd  8581  lesub1dd  8582  lesub2dd  8583  recexre  8599  apreap  8608  ltmul1a  8612  reapmul1  8616  cru  8623  apreim  8624  mulge0  8640  leltap  8646  negap0d  8652  ltleap  8653  ltapd  8659  ap0gt0  8661  ap0gt0d  8662  mulcanapad  8684  mulcanap2ad  8685  eqnegad  8755  diveqap0d  8818  diveqap1d  8819  divap1d  8822  rec11apd  8832  div11apd  8852  div2subap  8858  recgt0  8871  prodgt0  8873  lemul1a  8879  lemulge12  8888  lt2msq1  8906  lediv12a  8915  recreclt  8921  nn1suc  9003  nnnlt1  9010  nn2ge  9017  nn1gt1  9018  nnrecl  9241  nn0nlt0  9269  elnn0z  9333  nn0negleid  9388  elz2  9391  nn0n0n1ge2b  9399  nnm1ge0  9406  nn0ge0div  9407  zextle  9411  suprzclex  9418  nn0ind-raph  9437  zindd  9438  uzneg  9614  eluzadd  9624  eluzsub  9625  uzm1  9626  uz3m2nn  9641  supminfex  9665  infregelbex  9666  nn01to3  9685  irrmulap  9716  ltrec1d  9786  lerec2d  9787  ledivdivd  9791  divge1  9792  ltmul1dd  9821  ltmul2dd  9822  ltdiv1dd  9823  lediv1dd  9824  ltdiv23d  9826  lediv23d  9827  nn0ledivnn  9836  addlelt  9837  xrlelttr  9875  xrltletr  9876  xaddass2  9939  xltadd1  9945  xlt2add  9949  ixxdisj  9972  icoshftf1o  10060  icodisj  10061  lincmb01cmp  10072  iccf1o  10073  uzsubsubfz  10116  fzdisj  10121  fzopth  10130  fznatpl1  10145  fzsuc2  10148  fzp1disj  10149  fzrev2i  10155  uzdisj  10162  fseq1p1m1  10163  fzm1  10169  fzneuz  10170  fzp1nel  10173  fzrevral  10174  fznn0sub2  10197  fz0fzdiffz0  10199  difelfzle  10203  difelfznle  10204  nn0disj  10207  fzonnsub  10239  fzodisj  10248  fzouzdisj  10250  eluzgtdifelfzo  10267  ubmelfzo  10270  fzonn0p1p1  10283  ubmelm1fzo  10296  fzostep1  10307  exfzdc  10310  subfzo0  10312  qtri3or  10313  exbtwnzlemex  10321  rebtwn2z  10326  qbtwnrelemcalc  10327  qbtwnre  10328  qavgle  10330  apbtwnz  10346  flid  10356  flqwordi  10360  flqmulnn0  10371  flhalf  10374  flltdivnn0lt  10376  fldiv4p1lem1div2  10377  intfracq  10394  flqdiv  10395  flqpmodeq  10401  modqmulnn  10416  mulqaddmodid  10438  modqmuladdim  10441  modqmuladdnn0  10442  m1modge3gt1  10445  q2submod  10459  modaddmodup  10461  modqsubdir  10467  modqeqmodmin  10468  modfzo0difsn  10469  uzennn  10510  uzsinds  10518  monoord2  10560  ser3mono  10561  iseqf1olemqcl  10573  iseqf1olemnab  10575  iseqf1olemab  10576  iseqf1olemqf1o  10580  iseqf1olemqk  10581  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seq3f1olemqsum  10587  seq3f1olemp  10589  seqf1oglem1  10593  seqf1oglem2  10594  ser3le  10611  exp3val  10615  expnegap0  10621  expgt1  10651  ltexp2a  10665  le2sq2  10689  nnlesq  10717  qsqeqor  10724  bernneq  10734  expnbnd  10737  expnlbnd  10738  expnlbnd2  10739  expeq0d  10743  sq11d  10780  nn0ltexp2  10783  expcand  10791  nn0opthd  10796  facdiv  10812  faclbnd6  10818  facubnd  10819  facavg  10820  bcval4  10826  bcp1nk  10836  bcval5  10837  bcpasc  10840  hashennnuni  10853  isfinite4im  10866  hashnncl  10869  hashunlem  10878  fiprsshashgt1  10891  hashfzp1  10898  zfz1isolemiso  10913  seq3coll  10916  iswrdiz  10924  wrdffz  10938  seq3shft  10985  cjth  10993  cjdivap  11056  cjne0d  11094  cjap0d  11095  cvg1nlemcxze  11129  cvg1nlemcau  11131  cvg1nlemres  11132  recvguniq  11142  resqrexlemover  11157  resqrexlemdecn  11159  resqrexlemlo  11160  resqrexlemcalc2  11162  resqrexlemcalc3  11163  resqrexlemnmsq  11164  resqrexlemnm  11165  resqrexlemcvg  11166  resqrexlemglsq  11169  resqrexlemga  11170  leabs  11221  absrele  11230  nn0abscl  11232  ltabs  11234  abslt  11235  absle  11236  abstri  11251  amgm2  11265  sqr11d  11320  abs00d  11333  maxabsle  11351  maxabslemlub  11354  maxleastlt  11362  maxltsup  11365  2zsupmax  11372  minmax  11376  2zinfmin  11389  xrmaxleim  11390  xrmaxiflemlub  11394  xrmaxiflemcom  11395  xrmaxiflemval  11396  xrmaxleastlt  11402  xrmaxltsup  11404  xrmaxaddlem  11406  xrmaxadd  11407  xrminmax  11411  xrmin1inf  11413  xrmin2inf  11414  xrmineqinf  11415  climi  11433  reccn2ap  11459  climge0  11471  climle  11480  climserle  11491  climrecvg1n  11494  fz1f1o  11521  summodclem3  11526  summodclem2a  11527  summodc  11529  fisumss  11538  fsum0diaglem  11586  mptfzshft  11588  fsumrev  11589  fisum0diag2  11593  fsumlessfi  11606  fsumle  11609  fsumlt  11610  isumsplit  11637  isumrpcl  11640  expcnvap0  11648  geosergap  11652  pwm1geoserap1  11654  absgtap  11656  geolim  11657  geolim2  11658  georeclim  11659  geoisumr  11664  geoisum1c  11666  cvgratnnlembern  11669  cvgratnnlemseq  11672  cvgratnnlemsumlt  11674  cvgratnnlemfm  11675  cvgratnnlemrate  11676  cvgratnn  11677  cvgratz  11678  mertenslemub  11680  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  prodmodclem2a  11722  prodmodc  11724  zproddc  11725  fprodntrivap  11730  fprodf1o  11734  fprodssdc  11736  fprodsplitdc  11742  fprodrev  11765  fprodmodd  11787  efcllemp  11804  ege2le3  11817  eftlcvg  11833  eftlub  11836  efltim  11844  eflegeo  11847  tanaddap  11885  sinbnd  11898  cosbnd  11899  sin01bnd  11903  cos01bnd  11904  sinltxirr  11907  sin01gt0  11908  cos01gt0  11909  cos12dec  11914  eirraplem  11923  zdvdsdc  11958  dvdstr  11974  dvdsadd2b  11986  dvdslelemd  11988  divconjdvds  11994  alzdvds  11999  dvdsext  12000  fzm1ndvds  12001  fzo0dvdseq  12002  zeo3  12012  even2n  12018  mod2eq1n2dvds  12023  nn0ehalf  12047  nnehalf  12048  nno  12050  nn0oddm1d2  12053  divalglemnqt  12064  divalglemex  12066  divalglemeuneg  12067  divalg2  12070  divalgmod  12071  flodddiv4t2lthalf  12081  zsupcllemstep  12085  infssuzex  12089  zsupssdc  12094  dvdsbnd  12096  gcdsupex  12097  gcdsupcl  12098  gcddvds  12103  divgcdz  12111  divgcdnn  12115  gcd0id  12119  gcdneg  12122  gcd1  12127  dvdsgcdidd  12134  bezoutlemnewy  12136  bezoutlemstep  12137  bezoutlemmo  12146  bezoutlemsup  12149  dfgcd3  12150  bezout  12151  dfgcd2  12154  mulgcd  12156  sqgcd  12169  dvdssqlem  12170  bezoutr1  12173  uzwodc  12177  nninfctlemfo  12180  lcmval  12204  lcmcllem  12208  dvdslcm  12210  lcmgcdlem  12218  lcmdvds  12220  lcmgcdeq  12224  ncoprmgcdne1b  12230  mulgcddvds  12235  rpmulgcd2  12236  qredeu  12238  rpdvds  12240  prmind2  12261  nprm  12264  dvdsnprmd  12266  isprm5lem  12282  isprm5  12283  divgcdodd  12284  isprm6  12288  prmexpb  12292  pw2dvds  12307  pw2dvdseulemle  12308  oddpwdclemdc  12314  sqne2sq  12318  znege1  12319  sqrt2irraplemnn  12320  divnumden  12337  divdenle  12338  qden1elz  12346  nn0sqrtelqelz  12347  hashdvds  12362  crth  12365  phimullem  12366  eulerthlemfi  12369  eulerthlemh  12372  eulerthlemth  12373  eulerth  12374  prmdiv  12376  prmdiveq  12377  hashgcdlem  12379  phisum  12381  odzcllem  12383  odzdvds  12386  odzphi  12387  oddprm  12400  pythagtriplem3  12408  pythagtriplem4  12409  pythagtriplem10  12410  pythagtriplem11  12415  pythagtriplem13  12417  pythagtriplem19  12423  pcprendvds  12431  pcprendvds2  12432  pcpre1  12433  pcpremul  12434  pceulem  12435  pceu  12436  pczpre  12438  pcmul  12442  pcdiv  12443  pcqmul  12444  pcqdiv  12448  pcexp  12450  pcidlem  12464  pcneg  12466  pcdvdstr  12468  pcgcd1  12469  pc2dvds  12471  dvdsprmpweq  12476  dvdsprmpweqle  12478  pcaddlem  12480  pcadd  12481  pcadd2  12482  pcmpt  12484  fldivp1  12489  pcfaclem  12490  pcfac  12491  pcbc  12492  qexpz  12493  oddprmdvds  12495  pockthlem  12497  pockthg  12498  infpnlem2  12501  1arith  12508  4sqlem9  12527  4sqlem10  12528  4sqlem11  12542  4sqlem12  12543  4sqlem13m  12544  4sqlem14  12545  4sqlem16  12547  oddennn  12552  ennnfonelemk  12560  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemrnh  12576  ennnfonelemen  12581  ennnfonelemim  12584  ctinfomlemom  12587  ctiunctlemf  12598  ssnnctlemct  12606  nninfdclemcl  12608  nninfdclemp1  12610  nninfdclemlt  12611  unbendc  12614  mgmb1mgm1  12954  mgm1  12956  mgmidsssn0  12970  gsumfzval  12977  gsumress  12981  gsum0g  12982  gsumval2  12983  sgrp1  12997  sgrpidmndm  13004  ismndd  13021  mhmpropd  13041  resmhm  13062  resmhm2b  13064  gsumwsubmcl  13071  gsumwmhm  13073  isgrpd2e  13095  grpidd2  13116  isgrpinv  13129  grpinvinv  13142  grpidssd  13151  grpinvssd  13152  mulgval  13195  mulgfng  13197  mulgnegnn  13205  subg0  13253  issubg4m  13266  nsgconj  13279  1nsgtrivd  13292  eqgen  13300  eqgcpbl  13301  qus0  13308  ghmid  13322  resghm  13333  ghmnsgpreima  13342  kerf1ghm  13347  conjsubgen  13351  conjnmz  13352  imasabl  13409  rnglz  13444  rngrz  13445  qusrng  13457  issrgid  13480  srg1zr  13486  ringcl  13512  isringid  13524  ringcom  13530  ringpropd  13537  ringlz  13542  ringrz  13543  ring1  13558  opprrng  13576  opprring  13578  dvdsrcld  13596  unitcld  13607  unitmulcl  13612  unitgrp  13615  unitnegcl  13629  rhmmul  13663  isrhm2d  13664  rhmdvdsr  13674  rhmopp  13675  elrhmunit  13676  rhmunitinv  13677  subrgugrp  13739  aprsym  13783  islmodd  13792  lmod0vs  13820  lmodfopne  13825  lmodcom  13832  lssclg  13863  lspsnel5a  13909  lspsneq0b  13926  lsslsp  13928  sraring  13948  sralmod  13949  rspssp  13993  rnglidlmsgrp  13996  2idlcpblrng  14022  gsumfzfsumlem0  14085  zncrng  14144  znzrh2  14145  znzrhfo  14147  znf1o  14150  znfi  14154  znhash  14155  znidom  14156  znidomb  14157  znunit  14158  znrrg  14159  psrbaglesuppg  14169  psrelbas  14171  ntridm  14305  ntrtop  14307  ntrcls0  14310  ntr0  14313  isopn3i  14314  neiss2  14321  opnneiss  14337  topssnei  14341  cnpf2  14386  icnpimaex  14390  lmcvg  14396  iscnp4  14397  cncnp  14409  cnptopresti  14417  lmfss  14423  lmtopcnp  14429  hmeores  14494  bldisj  14580  xblss2ps  14583  xblss2  14584  blhalf  14587  blssps  14606  blss  14607  ssblex  14610  blpnfctr  14618  xmetresbl  14619  mopni2  14662  bdxmet  14680  bdbl  14682  xmetxpbl  14687  metcnpi  14694  metcnpi2  14695  tgioo  14733  rescncf  14760  mulcncflem  14786  cnopnap  14790  dedekindeulemuub  14796  dedekindeulemloc  14798  dedekindeulemlu  14800  dedekindeu  14802  dedekindicclemuub  14805  dedekindicclemloc  14807  dedekindicclemlu  14809  dedekindicclemicc  14811  dedekindicc  14812  ivthinclemlopn  14815  ivthinclemuopn  14817  ivthdec  14823  ivthreinc  14824  hovergt0  14829  dich0  14831  limcimolemlt  14843  cnplimcim  14846  cnplimclemr  14848  limccnpcntop  14854  limccnp2cntop  14856  limccoap  14857  dvfgg  14867  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvaddxxbr  14880  dvmulxxbr  14881  dvaddxx  14882  dvmulxx  14883  dviaddf  14884  dvimulf  14885  dvcoapbr  14886  dvcjbr  14887  dvcj  14888  dvrecap  14892  dvmptclx  14897  dveflem  14905  elply2  14914  plyf  14916  plyaddlem  14928  plymullem  14929  plyco  14937  plycj  14939  dvply1  14943  reeff1oleme  14948  eflt  14951  sin0pilem1  14957  pilem3  14959  cosq14gt0  15008  coseq0negpitopi  15012  tangtx  15014  coskpi  15024  cosordlem  15025  cosq34lt1  15026  relogef  15040  logrpap0d  15054  rplogcl  15055  logge0  15056  logdivlti  15057  cxplt3  15095  rpabscxpbnd  15114  lgslem1  15157  lgsval  15161  lgsfvalg  15162  lgsval2lem  15167  lgsvalmod  15176  lgsfcl3  15178  lgsmod  15183  lgsdirprm  15191  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  gausslemma2dlem0i  15214  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  gausslemma2dlem3  15220  gausslemma2dlem4  15221  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgseisen  15231  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem1  15238  lgsquad2lem2  15239  lgsquad3  15241  2lgslem1c  15247  2lgsoddprm  15270  2sqlem3  15274  2sqlem4  15275  2sqlem8  15280  bj-charfunr  15372  pwf1oexmid  15560  subctctexmid  15561  pw1nct  15563  nnsf  15565  peano4nninf  15566  nninfsellemeq  15574  cvgcmp2nlemabs  15592  iooref1o  15594  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  trirec0  15604  apdifflemf  15606  apdifflemr  15607  apdiff  15608  iswomninnlem  15609  redcwlpo  15615  redc0  15617  reap0  15618  nconstwlpolemgt0  15624  neapmkvlem  15627  ltlenmkv  15630  supfz  15631  inffz  15632