Theorem mpbid 146

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 143	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbii  147  annimdc  889  mpbi2and  895  bilukdc  1342  equs5or  1769  eqtrd  2132  eleqtrd  2178  neeqtrd  2295  3netr3d  2299  rexlimd2  2506  ceqsalt  2667  vtoclgft  2691  vtoclegft  2713  elrab3t  2792  eueq2dc  2810  sbceq1dd  2868  csbiedf  2990  sseqtrd  3085  3sstr3d  3091  ifbothdadc  3450  snssd  3612  dfnfc2  3701  breqtrd  3899  3brtr3d  3904  csbexga  3996  reuhypd  4330  reg2exmidlema  4387  elirr  4394  en2lp  4407  onsucuni2  4417  finds  4452  iota4  5042  iota4an  5043  funimaexglem  5142  fneu  5163  fco2  5225  fssres2  5236  fresin  5237  feu  5241  f1orescnv  5317  resdif  5323  funcocnv2  5326  f1oprg  5343  fvelrnb  5401  fimacnv  5481  f1oresrab  5517  fsn2  5526  xpsng  5527  fnressn  5538  fsnunf  5552  foeqcnvco  5623  isores1  5647  isoini2  5652  riota5f  5686  riotass2  5688  riotass  5689  ovmpodxf  5828  elopabi  6023  cnvf1o  6052  smores3  6120  tfrlemisucaccv  6152  tfr1onlemsucaccv  6168  tfrcllemsucaccv  6181  rdgon  6213  frecabcl  6226  frecsuclem  6233  nnsucsssuc  6318  nnsucuniel  6321  erref  6379  iserd  6385  swoer  6387  swoord1  6388  swoord2  6389  erth  6403  erthi  6405  eroveu  6450  pmresg  6500  mapsn  6514  fndmeng  6634  xpen  6668  phplem4  6678  phplem4on  6690  fidifsnen  6693  dif1en  6702  dif1enen  6703  fisbth  6706  diffisn  6716  ac6sfi  6721  fimax2gtri  6724  en2eqpr  6730  unsnfidcex  6737  unsnfidcel  6738  fiintim  6746  fidcenumlemrks  6769  eqsupti  6798  supisoti  6812  ordiso2  6835  casef  6888  difinfsnlem  6899  ctmlemr  6908  ctssdclemr  6911  enumct  6914  enomnilem  6922  exmidomni  6926  fodjum  6930  fodjuomnilemres  6932  mkvprop  6943  dfplpq2  7063  ltanqi  7111  ltmnqi  7112  ltaddnq  7116  subhalfnqq  7123  ltbtwnnqq  7124  archnqq  7126  prarloclemarch2  7128  enq0sym  7141  enq0ref  7142  enq0tr  7143  nqnq0pi  7147  nnnq0lem1  7155  distrnq0  7168  prarloclemlt  7202  prarloclemn  7208  prarloclemcalc  7211  genplt2i  7219  addnqprllem  7236  addnqprulem  7237  addlocprlemgt  7243  appdivnq  7272  prmuloc2  7276  ltexprlemopl  7310  ltexprlemopu  7312  ltexprlemru  7321  prplnqu  7329  cauappcvgprlemopl  7355  cauappcvgprlemlol  7356  cauappcvgprlemladdfu  7363  cauappcvgprlemladdrl  7366  cauappcvgprlem1  7368  archrecnq  7372  archrecpr  7373  caucvgprlemk  7374  caucvgprlemnbj  7376  caucvgprlemm  7377  caucvgprlemopl  7378  caucvgprlemlol  7379  caucvgprlemladdfu  7386  caucvgprlemladdrl  7387  caucvgprlem1  7388  caucvgprprlemk  7392  caucvgprprlemnkeqj  7399  caucvgprprlemnbj  7402  caucvgprprlemml  7403  caucvgprprlemmu  7404  caucvgprprlemopl  7406  caucvgprprlemlol  7407  caucvgprprlemopu  7408  caucvgprprlemexbt  7415  caucvgprprlemexb  7416  caucvgprprlem1  7418  caucvgprprlem2  7419  prsrlem1  7438  addgt0sr  7471  srpospr  7478  prsrriota  7483  caucvgsrlemgt1  7490  caucvgsrlemoffgt1  7494  caucvgsr  7497  recriota  7575  lelttr  7723  ltletr  7724  ltnsymd  7753  lensymd  7755  cnegexlem3  7810  cnegex2  7812  addcanad  7819  addcan2ad  7820  negcon1ad  7939  negne0d  7942  negrebd  7943  subeq0d  7952  subne0ad  7955  neg11d  7956  subcand  7985  subcan2d  7986  ltadd2  8048  ltadd2dd  8051  add20  8103  ltnegcon1d  8153  ltnegcon2d  8154  lenegcon1d  8155  lenegcon2d  8156  subled  8176  lesubd  8177  ltsub23d  8178  ltsub13d  8179  ltadd1dd  8184  ltsub1dd  8185  ltsub2dd  8186  leadd1dd  8187  leadd2dd  8188  lesub1dd  8189  lesub2dd  8190  recexre  8206  apreap  8215  ltmul1a  8219  reapmul1  8223  cru  8230  apreim  8231  mulge0  8247  leltap  8253  ltleap  8259  ltapd  8265  ap0gt0  8267  ap0gt0d  8268  subap0d  8271  mulcanapad  8285  mulcanap2ad  8286  eqnegad  8355  diveqap0d  8418  diveqap1d  8419  divap1d  8422  rec11apd  8432  div11apd  8452  div2subap  8457  recgt0  8466  prodgt0  8468  lemul1a  8474  lemulge12  8483  lt2msq1  8501  lediv12a  8510  recreclt  8516  nn1suc  8597  nnnlt1  8604  nn2ge  8611  nn1gt1  8612  nnrecl  8827  nn0nlt0  8855  elnn0z  8919  elz2  8974  nn0n0n1ge2b  8982  nnm1ge0  8989  nn0ge0div  8990  zextle  8994  suprzclex  9001  nn0ind-raph  9020  zindd  9021  uzneg  9194  eluzadd  9204  eluzsub  9205  uzm1  9206  uz3m2nn  9218  supminfex  9242  nn01to3  9259  ltrec1d  9351  lerec2d  9352  ledivdivd  9356  divge1  9357  ltmul1dd  9386  ltmul2dd  9387  ltdiv1dd  9388  lediv1dd  9389  ltdiv23d  9391  lediv23d  9392  nn0ledivnn  9395  addlelt  9396  xrlelttr  9430  xrltletr  9431  xaddass2  9494  xltadd1  9500  xlt2add  9504  ixxdisj  9527  icoshftf1o  9615  icodisj  9616  lincmb01cmp  9627  iccf1o  9628  uzsubsubfz  9668  fzdisj  9673  fzopth  9682  fznatpl1  9697  fzsuc2  9700  fzp1disj  9701  fzrev2i  9707  uzdisj  9714  fseq1p1m1  9715  fzm1  9721  fzneuz  9722  fzp1nel  9725  fzrevral  9726  fznn0sub2  9746  fz0fzdiffz0  9748  difelfzle  9752  difelfznle  9753  nn0disj  9756  fzonnsub  9787  fzodisj  9796  fzouzdisj  9798  eluzgtdifelfzo  9815  ubmelfzo  9818  fzonn0p1p1  9831  ubmelm1fzo  9844  fzostep1  9855  exfzdc  9858  subfzo0  9860  qtri3or  9861  exbtwnzlemex  9868  rebtwn2z  9873  qbtwnrelemcalc  9874  qbtwnre  9875  qavgle  9877  apbtwnz  9888  flid  9898  flqwordi  9902  flqmulnn0  9913  flhalf  9916  flltdivnn0lt  9918  fldiv4p1lem1div2  9919  intfracq  9934  flqdiv  9935  flqpmodeq  9941  modqmulnn  9956  mulqaddmodid  9978  modqmuladdim  9981  modqmuladdnn0  9982  m1modge3gt1  9985  q2submod  9999  modaddmodup  10001  modqsubdir  10007  modqeqmodmin  10008  modfzo0difsn  10009  uzennn  10050  uzsinds  10056  monoord2  10091  ser3mono  10092  iseqf1olemqcl  10100  iseqf1olemnab  10102  iseqf1olemab  10103  iseqf1olemqf1o  10107  iseqf1olemqk  10108  seq3f1olemqsumkj  10112  seq3f1olemqsumk  10113  seq3f1olemqsum  10114  seq3f1olemp  10116  ser3le  10132  exp3val  10136  expnegap0  10142  expgt1  10172  ltexp2a  10186  le2sq2  10209  nnlesq  10237  bernneq  10253  expnbnd  10256  expnlbnd  10257  expnlbnd2  10258  expeq0d  10261  sq11d  10298  expcand  10305  nn0opthd  10309  facdiv  10325  faclbnd6  10331  facubnd  10332  facavg  10333  bcval4  10339  bcp1nk  10349  bcval5  10350  bcpasc  10353  hashennnuni  10366  focdmex  10374  isfinite4im  10380  hashnncl  10383  hashunlem  10391  fiprsshashgt1  10404  hashfzp1  10411  zfz1isolemiso  10423  seq3coll  10426  seq3shft  10451  cjth  10459  cjdivap  10522  cjne0d  10560  cjap0d  10561  cvg1nlemcxze  10594  cvg1nlemcau  10596  cvg1nlemres  10597  recvguniq  10607  resqrexlemover  10622  resqrexlemdecn  10624  resqrexlemlo  10625  resqrexlemcalc2  10627  resqrexlemcalc3  10628  resqrexlemnmsq  10629  resqrexlemnm  10630  resqrexlemcvg  10631  resqrexlemglsq  10634  resqrexlemga  10635  leabs  10686  absrele  10695  nn0abscl  10697  ltabs  10699  abslt  10700  absle  10701  abstri  10716  amgm2  10730  sqr11d  10785  abs00d  10798  maxabsle  10816  maxabslemlub  10819  maxleastlt  10827  maxltsup  10830  2zsupmax  10836  minmax  10840  xrmaxleim  10852  xrmaxiflemlub  10856  xrmaxiflemcom  10857  xrmaxiflemval  10858  xrmaxleastlt  10864  xrmaxltsup  10866  xrmaxaddlem  10868  xrmaxadd  10869  xrminmax  10873  xrmin1inf  10875  xrmin2inf  10876  xrmineqinf  10877  climi  10895  reccn2ap  10921  climge0  10933  climle  10942  climserle  10953  climrecvg1n  10956  fz1f1o  10983  summodclem3  10988  summodclem2a  10989  summodc  10991  fisumss  11000  fsum0diaglem  11048  mptfzshft  11050  fsumrev  11051  fisum0diag2  11055  fsumlessfi  11068  fsumle  11071  fsumlt  11072  isumsplit  11099  isumrpcl  11102  expcnvap0  11110  geosergap  11114  pwm1geoserap1  11116  absgtap  11118  geolim  11119  geolim2  11120  georeclim  11121  geoisumr  11126  geoisum1c  11128  cvgratnnlembern  11131  cvgratnnlemseq  11134  cvgratnnlemsumlt  11136  cvgratnnlemfm  11137  cvgratnnlemrate  11138  cvgratnn  11139  cvgratz  11140  mertenslemub  11142  mertenslemi1  11143  mertenslem2  11144  mertensabs  11145  efcllemp  11162  ege2le3  11175  eftlcvg  11191  eftlub  11194  efltim  11202  eflegeo  11206  tanaddap  11244  sinbnd  11257  cosbnd  11258  sin01bnd  11262  cos01bnd  11263  sin01gt0  11266  cos01gt0  11267  eirraplem  11278  zdvdsdc  11309  dvdstr  11325  dvdsadd2b  11335  dvdslelemd  11336  divconjdvds  11342  alzdvds  11347  dvdsext  11348  fzm1ndvds  11349  fzo0dvdseq  11350  zeo3  11360  even2n  11366  mod2eq1n2dvds  11371  nn0ehalf  11395  nnehalf  11396  nno  11398  nn0oddm1d2  11401  divalglemnqt  11412  divalglemex  11414  divalglemeuneg  11415  divalg2  11418  divalgmod  11419  flodddiv4t2lthalf  11429  zsupcllemstep  11433  infssuzex  11437  dvdsbnd  11440  gcdsupex  11441  gcdsupcl  11442  gcddvds  11447  divgcdz  11455  divgcdnn  11458  gcd0id  11462  gcdneg  11465  gcd1  11470  bezoutlemnewy  11477  bezoutlemstep  11478  bezoutlemmo  11487  bezoutlemsup  11490  dfgcd3  11491  bezout  11492  dfgcd2  11495  mulgcd  11497  sqgcd  11510  dvdssqlem  11511  bezoutr1  11514  lcmval  11537  lcmcllem  11541  dvdslcm  11543  lcmgcdlem  11551  lcmdvds  11553  lcmgcdeq  11557  ncoprmgcdne1b  11563  mulgcddvds  11568  rpmulgcd2  11569  qredeu  11571  rpdvds  11573  prmind2  11594  nprm  11597  dvdsnprmd  11599  divgcdodd  11614  isprm6  11618  prmexpb  11622  pw2dvds  11636  pw2dvdseulemle  11637  oddpwdclemdc  11643  sqne2sq  11647  znege1  11648  sqrt2irraplemnn  11649  divnumden  11666  divdenle  11667  qden1elz  11675  nn0sqrtelqelz  11676  hashdvds  11689  crth  11692  phimullem  11693  hashgcdlem  11695  oddennn  11697  ennnfonelemk  11705  ennnfonelemkh  11717  ennnfonelemhf1o  11718  ennnfonelemex  11719  ennnfonelemhom  11720  ennnfonelemrnh  11721  ennnfonelemen  11726  ennnfonelemim  11729  ctinfomlemom  11732  ntridm  12077  ntrtop  12079  ntrcls0  12082  ntr0  12085  isopn3i  12086  neiss2  12093  opnneiss  12109  topssnei  12113  cnpf2  12157  icnpimaex  12161  lmcvg  12167  iscnp4  12168  cncnp  12180  cnptopresti  12188  lmfss  12194  lmtopcnp  12200  bldisj  12329  xblss2ps  12332  xblss2  12333  blhalf  12336  blssps  12355  blss  12356  ssblex  12359  blpnfctr  12367  xmetresbl  12368  mopni2  12411  bdxmet  12429  bdbl  12431  metcnpi  12439  metcnpi2  12440  tgioo  12465  rescncf  12481  mulcncflem  12502  limcimolemlt  12513  cnplimcim  12516  limccnpcntop  12520  dvfgg  12530  dvidlemap  12533  pwf1oexmid  12780  nnsf  12783  peano4nninf  12784  nninfalllemn  12786  nninfsellemeq  12794  cvgcmp2nlemabs  12811  trilpolemisumle  12815  trilpolemeq1  12817  trilpolemlt1  12818  supfz  12821  inffz  12822