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  2810  vtoclegft  2832  elrab3t  2915  eueq2dc  2933  sbceq1dd  2991  csbiedf  3121  sseqtrd  3217  3sstr3d  3223  ifbothdadc  3589  snssd  3763  dfnfc2  3853  breqdi  4044  breqtrd  4055  3brtr3d  4060  csbexga  4157  reuhypd  4502  reg2exmidlema  4566  elirr  4573  en2lp  4586  onsucuni2  4596  finds  4632  iota4  5234  iota4an  5235  funimaexglem  5337  fneu  5358  fco2  5420  fssres2  5431  fresin  5432  feu  5436  f1orescnv  5516  resdif  5522  funcocnv2  5525  f1oprg  5544  fvelrnb  5604  fimacnv  5687  f1oresrab  5723  fsn2  5732  xpsng  5733  fnressn  5744  fsnunf  5758  foeqcnvco  5833  isores1  5857  isoini2  5862  riota5f  5898  riotass2  5900  riotass  5901  ovmpodxf  6044  uchoice  6190  elopabi  6248  cnvf1o  6278  smores3  6346  tfrlemisucaccv  6378  tfr1onlemsucaccv  6394  tfrcllemsucaccv  6407  rdgon  6439  frecabcl  6452  frecsuclem  6459  nnsucsssuc  6545  nnsucuniel  6548  erref  6607  iserd  6613  swoer  6615  swoord1  6616  swoord2  6617  erth  6633  erthi  6635  eroveu  6680  pmresg  6730  mapsn  6744  fndmeng  6864  xpen  6901  phplem4  6911  phplem4on  6923  fidifsnen  6926  dif1en  6935  dif1enen  6936  fisbth  6939  diffisn  6949  ac6sfi  6954  fimax2gtri  6957  en2eqpr  6963  unsnfidcex  6976  unsnfidcel  6977  fiintim  6985  fidcenumlemrks  7012  elfi2  7031  elfir  7032  fiuni  7037  fifo  7039  eqsupti  7055  supisoti  7069  ordiso2  7094  casef  7147  difinfsnlem  7158  ctmlemr  7167  ctssdccl  7170  enumct  7174  nninfninc  7182  nnnninfeq  7187  nnnninfeq2  7188  enomnilem  7197  exmidomni  7201  fodjum  7205  fodjuomnilemres  7207  mkvprop  7217  enmkvlem  7220  enwomnilem  7228  nninfdcinf  7230  nninfwlpoimlemdc  7236  acfun  7267  2omotaplemap  7317  exmidmotap  7321  ccfunen  7324  cc2lem  7326  dfplpq2  7414  ltanqi  7462  ltmnqi  7463  ltaddnq  7467  subhalfnqq  7474  ltbtwnnqq  7475  archnqq  7477  prarloclemarch2  7479  enq0sym  7492  enq0ref  7493  enq0tr  7494  nqnq0pi  7498  nnnq0lem1  7506  distrnq0  7519  prarloclemlt  7553  prarloclemn  7559  prarloclemcalc  7562  genplt2i  7570  addnqprllem  7587  addnqprulem  7588  addlocprlemgt  7594  appdivnq  7623  prmuloc2  7627  ltexprlemopl  7661  ltexprlemopu  7663  ltexprlemru  7672  prplnqu  7680  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemladdfu  7714  cauappcvgprlemladdrl  7717  cauappcvgprlem1  7719  archrecnq  7723  archrecpr  7724  caucvgprlemk  7725  caucvgprlemnbj  7727  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  caucvgprlem1  7739  caucvgprprlemk  7743  caucvgprprlemnkeqj  7750  caucvgprprlemnbj  7753  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemopu  7759  caucvgprprlemexbt  7766  caucvgprprlemexb  7767  caucvgprprlem1  7769  caucvgprprlem2  7770  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemub  7783  suplocexprlemlub  7784  prsrlem1  7802  addgt0sr  7835  srpospr  7843  prsrriota  7848  caucvgsrlemgt1  7855  caucvgsrlemoffgt1  7859  caucvgsr  7862  mappsrprg  7864  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  recriota  7950  axsuploc  8092  lelttr  8108  ltletr  8109  ltnsymd  8139  lensymd  8141  cnegexlem3  8196  cnegex2  8198  addcanad  8205  addcan2ad  8206  negcon1ad  8325  negne0d  8328  negrebd  8329  subeq0d  8338  subne0ad  8341  neg11d  8342  subcand  8371  subcan2d  8372  ltadd2  8438  ltadd2dd  8441  add20  8493  ltnegcon1d  8544  ltnegcon2d  8545  lenegcon1d  8546  lenegcon2d  8547  subled  8567  lesubd  8568  ltsub23d  8569  ltsub13d  8570  ltadd1dd  8575  ltsub1dd  8576  ltsub2dd  8577  leadd1dd  8578  leadd2dd  8579  lesub1dd  8580  lesub2dd  8581  recexre  8597  apreap  8606  ltmul1a  8610  reapmul1  8614  cru  8621  apreim  8622  mulge0  8638  leltap  8644  negap0d  8650  ltleap  8651  ltapd  8657  ap0gt0  8659  ap0gt0d  8660  mulcanapad  8682  mulcanap2ad  8683  eqnegad  8753  diveqap0d  8816  diveqap1d  8817  divap1d  8820  rec11apd  8830  div11apd  8850  div2subap  8856  recgt0  8869  prodgt0  8871  lemul1a  8877  lemulge12  8886  lt2msq1  8904  lediv12a  8913  recreclt  8919  nn1suc  9001  nnnlt1  9008  nn2ge  9015  nn1gt1  9016  nnrecl  9238  nn0nlt0  9266  elnn0z  9330  nn0negleid  9385  elz2  9388  nn0n0n1ge2b  9396  nnm1ge0  9403  nn0ge0div  9404  zextle  9408  suprzclex  9415  nn0ind-raph  9434  zindd  9435  uzneg  9611  eluzadd  9621  eluzsub  9622  uzm1  9623  uz3m2nn  9638  supminfex  9662  infregelbex  9663  nn01to3  9682  irrmulap  9713  ltrec1d  9783  lerec2d  9784  ledivdivd  9788  divge1  9789  ltmul1dd  9818  ltmul2dd  9819  ltdiv1dd  9820  lediv1dd  9821  ltdiv23d  9823  lediv23d  9824  nn0ledivnn  9833  addlelt  9834  xrlelttr  9872  xrltletr  9873  xaddass2  9936  xltadd1  9942  xlt2add  9946  ixxdisj  9969  icoshftf1o  10057  icodisj  10058  lincmb01cmp  10069  iccf1o  10070  uzsubsubfz  10113  fzdisj  10118  fzopth  10127  fznatpl1  10142  fzsuc2  10145  fzp1disj  10146  fzrev2i  10152  uzdisj  10159  fseq1p1m1  10160  fzm1  10166  fzneuz  10167  fzp1nel  10170  fzrevral  10171  fznn0sub2  10194  fz0fzdiffz0  10196  difelfzle  10200  difelfznle  10201  nn0disj  10204  fzonnsub  10236  fzodisj  10245  fzouzdisj  10247  eluzgtdifelfzo  10264  ubmelfzo  10267  fzonn0p1p1  10280  ubmelm1fzo  10293  fzostep1  10304  exfzdc  10307  subfzo0  10309  qtri3or  10310  exbtwnzlemex  10318  rebtwn2z  10323  qbtwnrelemcalc  10324  qbtwnre  10325  qavgle  10327  apbtwnz  10343  flid  10353  flqwordi  10357  flqmulnn0  10368  flhalf  10371  flltdivnn0lt  10373  fldiv4p1lem1div2  10374  intfracq  10391  flqdiv  10392  flqpmodeq  10398  modqmulnn  10413  mulqaddmodid  10435  modqmuladdim  10438  modqmuladdnn0  10439  m1modge3gt1  10442  q2submod  10456  modaddmodup  10458  modqsubdir  10464  modqeqmodmin  10465  modfzo0difsn  10466  uzennn  10507  uzsinds  10515  monoord2  10557  ser3mono  10558  iseqf1olemqcl  10570  iseqf1olemnab  10572  iseqf1olemab  10573  iseqf1olemqf1o  10577  iseqf1olemqk  10578  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  seq3f1olemp  10586  seqf1oglem1  10590  seqf1oglem2  10591  ser3le  10608  exp3val  10612  expnegap0  10618  expgt1  10648  ltexp2a  10662  le2sq2  10686  nnlesq  10714  qsqeqor  10721  bernneq  10731  expnbnd  10734  expnlbnd  10735  expnlbnd2  10736  expeq0d  10740  sq11d  10777  nn0ltexp2  10780  expcand  10788  nn0opthd  10793  facdiv  10809  faclbnd6  10815  facubnd  10816  facavg  10817  bcval4  10823  bcp1nk  10833  bcval5  10834  bcpasc  10837  hashennnuni  10850  isfinite4im  10863  hashnncl  10866  hashunlem  10875  fiprsshashgt1  10888  hashfzp1  10895  zfz1isolemiso  10910  seq3coll  10913  iswrdiz  10921  wrdffz  10935  seq3shft  10982  cjth  10990  cjdivap  11053  cjne0d  11091  cjap0d  11092  cvg1nlemcxze  11126  cvg1nlemcau  11128  cvg1nlemres  11129  recvguniq  11139  resqrexlemover  11154  resqrexlemdecn  11156  resqrexlemlo  11157  resqrexlemcalc2  11159  resqrexlemcalc3  11160  resqrexlemnmsq  11161  resqrexlemnm  11162  resqrexlemcvg  11163  resqrexlemglsq  11166  resqrexlemga  11167  leabs  11218  absrele  11227  nn0abscl  11229  ltabs  11231  abslt  11232  absle  11233  abstri  11248  amgm2  11262  sqr11d  11317  abs00d  11330  maxabsle  11348  maxabslemlub  11351  maxleastlt  11359  maxltsup  11362  2zsupmax  11369  minmax  11373  2zinfmin  11386  xrmaxleim  11387  xrmaxiflemlub  11391  xrmaxiflemcom  11392  xrmaxiflemval  11393  xrmaxleastlt  11399  xrmaxltsup  11401  xrmaxaddlem  11403  xrmaxadd  11404  xrminmax  11408  xrmin1inf  11410  xrmin2inf  11411  xrmineqinf  11412  climi  11430  reccn2ap  11456  climge0  11468  climle  11477  climserle  11488  climrecvg1n  11491  fz1f1o  11518  summodclem3  11523  summodclem2a  11524  summodc  11526  fisumss  11535  fsum0diaglem  11583  mptfzshft  11585  fsumrev  11586  fisum0diag2  11590  fsumlessfi  11603  fsumle  11606  fsumlt  11607  isumsplit  11634  isumrpcl  11637  expcnvap0  11645  geosergap  11649  pwm1geoserap1  11651  absgtap  11653  geolim  11654  geolim2  11655  georeclim  11656  geoisumr  11661  geoisum1c  11663  cvgratnnlembern  11666  cvgratnnlemseq  11669  cvgratnnlemsumlt  11671  cvgratnnlemfm  11672  cvgratnnlemrate  11673  cvgratnn  11674  cvgratz  11675  mertenslemub  11677  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  prodmodclem2a  11719  prodmodc  11721  zproddc  11722  fprodntrivap  11727  fprodf1o  11731  fprodssdc  11733  fprodsplitdc  11739  fprodrev  11762  fprodmodd  11784  efcllemp  11801  ege2le3  11814  eftlcvg  11830  eftlub  11833  efltim  11841  eflegeo  11844  tanaddap  11882  sinbnd  11895  cosbnd  11896  sin01bnd  11900  cos01bnd  11901  sinltxirr  11904  sin01gt0  11905  cos01gt0  11906  cos12dec  11911  eirraplem  11920  zdvdsdc  11955  dvdstr  11971  dvdsadd2b  11983  dvdslelemd  11985  divconjdvds  11991  alzdvds  11996  dvdsext  11997  fzm1ndvds  11998  fzo0dvdseq  11999  zeo3  12009  even2n  12015  mod2eq1n2dvds  12020  nn0ehalf  12044  nnehalf  12045  nno  12047  nn0oddm1d2  12050  divalglemnqt  12061  divalglemex  12063  divalglemeuneg  12064  divalg2  12067  divalgmod  12068  flodddiv4t2lthalf  12078  zsupcllemstep  12082  infssuzex  12086  zsupssdc  12091  dvdsbnd  12093  gcdsupex  12094  gcdsupcl  12095  gcddvds  12100  divgcdz  12108  divgcdnn  12112  gcd0id  12116  gcdneg  12119  gcd1  12124  dvdsgcdidd  12131  bezoutlemnewy  12133  bezoutlemstep  12134  bezoutlemmo  12143  bezoutlemsup  12146  dfgcd3  12147  bezout  12148  dfgcd2  12151  mulgcd  12153  sqgcd  12166  dvdssqlem  12167  bezoutr1  12170  uzwodc  12174  nninfctlemfo  12177  lcmval  12201  lcmcllem  12205  dvdslcm  12207  lcmgcdlem  12215  lcmdvds  12217  lcmgcdeq  12221  ncoprmgcdne1b  12227  mulgcddvds  12232  rpmulgcd2  12233  qredeu  12235  rpdvds  12237  prmind2  12258  nprm  12261  dvdsnprmd  12263  isprm5lem  12279  isprm5  12280  divgcdodd  12281  isprm6  12285  prmexpb  12289  pw2dvds  12304  pw2dvdseulemle  12305  oddpwdclemdc  12311  sqne2sq  12315  znege1  12316  sqrt2irraplemnn  12317  divnumden  12334  divdenle  12335  qden1elz  12343  nn0sqrtelqelz  12344  hashdvds  12359  crth  12362  phimullem  12363  eulerthlemfi  12366  eulerthlemh  12369  eulerthlemth  12370  eulerth  12371  prmdiv  12373  prmdiveq  12374  hashgcdlem  12376  phisum  12378  odzcllem  12380  odzdvds  12383  odzphi  12384  oddprm  12397  pythagtriplem3  12405  pythagtriplem4  12406  pythagtriplem10  12407  pythagtriplem11  12412  pythagtriplem13  12414  pythagtriplem19  12420  pcprendvds  12428  pcprendvds2  12429  pcpre1  12430  pcpremul  12431  pceulem  12432  pceu  12433  pczpre  12435  pcmul  12439  pcdiv  12440  pcqmul  12441  pcqdiv  12445  pcexp  12447  pcidlem  12461  pcneg  12463  pcdvdstr  12465  pcgcd1  12466  pc2dvds  12468  dvdsprmpweq  12473  dvdsprmpweqle  12475  pcaddlem  12477  pcadd  12478  pcadd2  12479  pcmpt  12481  fldivp1  12486  pcfaclem  12487  pcfac  12488  pcbc  12489  qexpz  12490  oddprmdvds  12492  pockthlem  12494  pockthg  12495  infpnlem2  12498  1arith  12505  4sqlem9  12524  4sqlem10  12525  4sqlem11  12539  4sqlem12  12540  4sqlem13m  12541  4sqlem14  12542  4sqlem16  12544  oddennn  12549  ennnfonelemk  12557  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemrnh  12573  ennnfonelemen  12578  ennnfonelemim  12581  ctinfomlemom  12584  ctiunctlemf  12595  ssnnctlemct  12603  nninfdclemcl  12605  nninfdclemp1  12607  nninfdclemlt  12608  unbendc  12611  mgmb1mgm1  12951  mgm1  12953  mgmidsssn0  12967  gsumfzval  12974  gsumress  12978  gsum0g  12979  gsumval2  12980  sgrp1  12994  sgrpidmndm  13001  ismndd  13018  mhmpropd  13038  resmhm  13059  resmhm2b  13061  gsumwsubmcl  13068  gsumwmhm  13070  isgrpd2e  13092  grpidd2  13113  isgrpinv  13126  grpinvinv  13139  grpidssd  13148  grpinvssd  13149  mulgval  13192  mulgfng  13194  mulgnegnn  13202  subg0  13250  issubg4m  13263  nsgconj  13276  1nsgtrivd  13289  eqgen  13297  eqgcpbl  13298  qus0  13305  ghmid  13319  resghm  13330  ghmnsgpreima  13339  kerf1ghm  13344  conjsubgen  13348  conjnmz  13349  imasabl  13406  rnglz  13441  rngrz  13442  qusrng  13454  issrgid  13477  srg1zr  13483  ringcl  13509  isringid  13521  ringcom  13527  ringpropd  13534  ringlz  13539  ringrz  13540  ring1  13555  opprrng  13573  opprring  13575  dvdsrcld  13593  unitcld  13604  unitmulcl  13609  unitgrp  13612  unitnegcl  13626  rhmmul  13660  isrhm2d  13661  rhmdvdsr  13671  rhmopp  13672  elrhmunit  13673  rhmunitinv  13674  subrgugrp  13736  aprsym  13780  islmodd  13789  lmod0vs  13817  lmodfopne  13822  lmodcom  13829  lssclg  13860  lspsnel5a  13906  lspsneq0b  13923  lsslsp  13925  sraring  13945  sralmod  13946  rspssp  13990  rnglidlmsgrp  13993  2idlcpblrng  14019  gsumfzfsumlem0  14074  zncrng  14133  znzrh2  14134  znzrhfo  14136  znf1o  14139  znfi  14143  znhash  14144  znidom  14145  znidomb  14146  znunit  14147  znrrg  14148  psrbaglesuppg  14158  psrelbas  14160  ntridm  14294  ntrtop  14296  ntrcls0  14299  ntr0  14302  isopn3i  14303  neiss2  14310  opnneiss  14326  topssnei  14330  cnpf2  14375  icnpimaex  14379  lmcvg  14385  iscnp4  14386  cncnp  14398  cnptopresti  14406  lmfss  14412  lmtopcnp  14418  hmeores  14483  bldisj  14569  xblss2ps  14572  xblss2  14573  blhalf  14576  blssps  14595  blss  14596  ssblex  14599  blpnfctr  14607  xmetresbl  14608  mopni2  14651  bdxmet  14669  bdbl  14671  xmetxpbl  14676  metcnpi  14683  metcnpi2  14684  tgioo  14714  rescncf  14736  mulcncflem  14761  cnopnap  14765  dedekindeulemuub  14771  dedekindeulemloc  14773  dedekindeulemlu  14775  dedekindeu  14777  dedekindicclemuub  14780  dedekindicclemloc  14782  dedekindicclemlu  14784  dedekindicclemicc  14786  dedekindicc  14787  ivthinclemlopn  14790  ivthinclemuopn  14792  ivthdec  14798  ivthreinc  14799  hovergt0  14804  dich0  14806  limcimolemlt  14818  cnplimcim  14821  cnplimclemr  14823  limccnpcntop  14829  limccnp2cntop  14831  limccoap  14832  dvfgg  14842  dvidlemap  14845  dvaddxxbr  14850  dvmulxxbr  14851  dvaddxx  14852  dvmulxx  14853  dviaddf  14854  dvimulf  14855  dvcoapbr  14856  dvcjbr  14857  dvcj  14858  dvrecap  14862  dvmptclx  14865  dveflem  14872  elply2  14881  plyf  14883  plyaddlem  14895  plymullem  14896  reeff1oleme  14907  eflt  14910  sin0pilem1  14916  pilem3  14918  cosq14gt0  14967  coseq0negpitopi  14971  tangtx  14973  coskpi  14983  cosordlem  14984  cosq34lt1  14985  relogef  14999  logrpap0d  15013  rplogcl  15014  logge0  15015  logdivlti  15016  cxplt3  15054  rpabscxpbnd  15073  lgslem1  15116  lgsval  15120  lgsfvalg  15121  lgsval2lem  15126  lgsvalmod  15135  lgsfcl3  15137  lgsmod  15142  lgsdirprm  15150  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  gausslemma2dlem0i  15173  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  gausslemma2dlem3  15179  gausslemma2dlem4  15180  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  lgseisen  15190  lgsquadlem1  15191  2sqlem3  15204  2sqlem4  15205  2sqlem8  15210  bj-charfunr  15302  pwf1oexmid  15490  subctctexmid  15491  pw1nct  15493  nnsf  15495  peano4nninf  15496  nninfsellemeq  15504  cvgcmp2nlemabs  15522  iooref1o  15524  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  trirec0  15534  apdifflemf  15536  apdifflemr  15537  apdiff  15538  iswomninnlem  15539  redcwlpo  15545  redc0  15547  reap0  15548  nconstwlpolemgt0  15554  neapmkvlem  15557  ltlenmkv  15560  supfz  15561  inffz  15562