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-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbii  147  annimdc  922  mpbi2and  928  bilukdc  1375  equs5or  1803  eqtrd  2173  eleqtrd  2219  neeqtrd  2337  3netr3d  2341  rexlimd2  2550  ceqsalt  2715  vtoclgft  2739  vtoclegft  2761  elrab3t  2843  eueq2dc  2861  sbceq1dd  2919  csbiedf  3045  sseqtrd  3140  3sstr3d  3146  ifbothdadc  3508  snssd  3673  dfnfc2  3762  breqdi  3952  breqtrd  3962  3brtr3d  3967  csbexga  4064  reuhypd  4400  reg2exmidlema  4457  elirr  4464  en2lp  4477  onsucuni2  4487  finds  4522  iota4  5114  iota4an  5115  funimaexglem  5214  fneu  5235  fco2  5297  fssres2  5308  fresin  5309  feu  5313  f1orescnv  5391  resdif  5397  funcocnv2  5400  f1oprg  5419  fvelrnb  5477  fimacnv  5557  f1oresrab  5593  fsn2  5602  xpsng  5603  fnressn  5614  fsnunf  5628  foeqcnvco  5699  isores1  5723  isoini2  5728  riota5f  5762  riotass2  5764  riotass  5765  ovmpodxf  5904  elopabi  6101  cnvf1o  6130  smores3  6198  tfrlemisucaccv  6230  tfr1onlemsucaccv  6246  tfrcllemsucaccv  6259  rdgon  6291  frecabcl  6304  frecsuclem  6311  nnsucsssuc  6396  nnsucuniel  6399  erref  6457  iserd  6463  swoer  6465  swoord1  6466  swoord2  6467  erth  6481  erthi  6483  eroveu  6528  pmresg  6578  mapsn  6592  fndmeng  6712  xpen  6747  phplem4  6757  phplem4on  6769  fidifsnen  6772  dif1en  6781  dif1enen  6782  fisbth  6785  diffisn  6795  ac6sfi  6800  fimax2gtri  6803  en2eqpr  6809  unsnfidcex  6816  unsnfidcel  6817  fiintim  6825  fidcenumlemrks  6849  elfi2  6868  elfir  6869  fiuni  6874  fifo  6876  eqsupti  6891  supisoti  6905  ordiso2  6928  casef  6981  difinfsnlem  6992  ctmlemr  7001  ctssdccl  7004  enumct  7008  enomnilem  7018  exmidomni  7022  fodjum  7026  fodjuomnilemres  7028  mkvprop  7040  enmkvlem  7043  enwomnilem  7050  acfun  7080  ccfunen  7096  cc2lem  7098  dfplpq2  7186  ltanqi  7234  ltmnqi  7235  ltaddnq  7239  subhalfnqq  7246  ltbtwnnqq  7247  archnqq  7249  prarloclemarch2  7251  enq0sym  7264  enq0ref  7265  enq0tr  7266  nqnq0pi  7270  nnnq0lem1  7278  distrnq0  7291  prarloclemlt  7325  prarloclemn  7331  prarloclemcalc  7334  genplt2i  7342  addnqprllem  7359  addnqprulem  7360  addlocprlemgt  7366  appdivnq  7395  prmuloc2  7399  ltexprlemopl  7433  ltexprlemopu  7435  ltexprlemru  7444  prplnqu  7452  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemladdfu  7486  cauappcvgprlemladdrl  7489  cauappcvgprlem1  7491  archrecnq  7495  archrecpr  7496  caucvgprlemk  7497  caucvgprlemnbj  7499  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprlem1  7511  caucvgprprlemk  7515  caucvgprprlemnkeqj  7522  caucvgprprlemnbj  7525  caucvgprprlemml  7526  caucvgprprlemmu  7527  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemopu  7531  caucvgprprlemexbt  7538  caucvgprprlemexb  7539  caucvgprprlem1  7541  caucvgprprlem2  7542  suplocexprlemru  7551  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemub  7555  suplocexprlemlub  7556  prsrlem1  7574  addgt0sr  7607  srpospr  7615  prsrriota  7620  caucvgsrlemgt1  7627  caucvgsrlemoffgt1  7631  caucvgsr  7634  mappsrprg  7636  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  recriota  7722  axsuploc  7861  lelttr  7876  ltletr  7877  ltnsymd  7906  lensymd  7908  cnegexlem3  7963  cnegex2  7965  addcanad  7972  addcan2ad  7973  negcon1ad  8092  negne0d  8095  negrebd  8096  subeq0d  8105  subne0ad  8108  neg11d  8109  subcand  8138  subcan2d  8139  ltadd2  8205  ltadd2dd  8208  add20  8260  ltnegcon1d  8311  ltnegcon2d  8312  lenegcon1d  8313  lenegcon2d  8314  subled  8334  lesubd  8335  ltsub23d  8336  ltsub13d  8337  ltadd1dd  8342  ltsub1dd  8343  ltsub2dd  8344  leadd1dd  8345  leadd2dd  8346  lesub1dd  8347  lesub2dd  8348  recexre  8364  apreap  8373  ltmul1a  8377  reapmul1  8381  cru  8388  apreim  8389  mulge0  8405  leltap  8411  negap0d  8417  ltleap  8418  ltapd  8424  ap0gt0  8426  ap0gt0d  8427  subap0d  8430  mulcanapad  8448  mulcanap2ad  8449  eqnegad  8518  diveqap0d  8581  diveqap1d  8582  divap1d  8585  rec11apd  8595  div11apd  8615  div2subap  8620  recgt0  8632  prodgt0  8634  lemul1a  8640  lemulge12  8649  lt2msq1  8667  lediv12a  8676  recreclt  8682  nn1suc  8763  nnnlt1  8770  nn2ge  8777  nn1gt1  8778  nnrecl  8999  nn0nlt0  9027  elnn0z  9091  elz2  9146  nn0n0n1ge2b  9154  nnm1ge0  9161  nn0ge0div  9162  zextle  9166  suprzclex  9173  nn0ind-raph  9192  zindd  9193  uzneg  9368  eluzadd  9378  eluzsub  9379  uzm1  9380  uz3m2nn  9395  supminfex  9419  nn01to3  9436  ltrec1d  9534  lerec2d  9535  ledivdivd  9539  divge1  9540  ltmul1dd  9569  ltmul2dd  9570  ltdiv1dd  9571  lediv1dd  9572  ltdiv23d  9574  lediv23d  9575  nn0ledivnn  9584  addlelt  9585  xrlelttr  9619  xrltletr  9620  xaddass2  9683  xltadd1  9689  xlt2add  9693  ixxdisj  9716  icoshftf1o  9804  icodisj  9805  lincmb01cmp  9816  iccf1o  9817  uzsubsubfz  9858  fzdisj  9863  fzopth  9872  fznatpl1  9887  fzsuc2  9890  fzp1disj  9891  fzrev2i  9897  uzdisj  9904  fseq1p1m1  9905  fzm1  9911  fzneuz  9912  fzp1nel  9915  fzrevral  9916  fznn0sub2  9936  fz0fzdiffz0  9938  difelfzle  9942  difelfznle  9943  nn0disj  9946  fzonnsub  9977  fzodisj  9986  fzouzdisj  9988  eluzgtdifelfzo  10005  ubmelfzo  10008  fzonn0p1p1  10021  ubmelm1fzo  10034  fzostep1  10045  exfzdc  10048  subfzo0  10050  qtri3or  10051  exbtwnzlemex  10058  rebtwn2z  10063  qbtwnrelemcalc  10064  qbtwnre  10065  qavgle  10067  apbtwnz  10078  flid  10088  flqwordi  10092  flqmulnn0  10103  flhalf  10106  flltdivnn0lt  10108  fldiv4p1lem1div2  10109  intfracq  10124  flqdiv  10125  flqpmodeq  10131  modqmulnn  10146  mulqaddmodid  10168  modqmuladdim  10171  modqmuladdnn0  10172  m1modge3gt1  10175  q2submod  10189  modaddmodup  10191  modqsubdir  10197  modqeqmodmin  10198  modfzo0difsn  10199  uzennn  10240  uzsinds  10246  monoord2  10281  ser3mono  10282  iseqf1olemqcl  10290  iseqf1olemnab  10292  iseqf1olemab  10293  iseqf1olemqf1o  10297  iseqf1olemqk  10298  seq3f1olemqsumkj  10302  seq3f1olemqsumk  10303  seq3f1olemqsum  10304  seq3f1olemp  10306  ser3le  10322  exp3val  10326  expnegap0  10332  expgt1  10362  ltexp2a  10376  le2sq2  10399  nnlesq  10427  bernneq  10443  expnbnd  10446  expnlbnd  10447  expnlbnd2  10448  expeq0d  10451  sq11d  10488  expcand  10495  nn0opthd  10500  facdiv  10516  faclbnd6  10522  facubnd  10523  facavg  10524  bcval4  10530  bcp1nk  10540  bcval5  10541  bcpasc  10544  hashennnuni  10557  focdmex  10565  isfinite4im  10571  hashnncl  10574  hashunlem  10582  fiprsshashgt1  10595  hashfzp1  10602  zfz1isolemiso  10614  seq3coll  10617  seq3shft  10642  cjth  10650  cjdivap  10713  cjne0d  10751  cjap0d  10752  cvg1nlemcxze  10786  cvg1nlemcau  10788  cvg1nlemres  10789  recvguniq  10799  resqrexlemover  10814  resqrexlemdecn  10816  resqrexlemlo  10817  resqrexlemcalc2  10819  resqrexlemcalc3  10820  resqrexlemnmsq  10821  resqrexlemnm  10822  resqrexlemcvg  10823  resqrexlemglsq  10826  resqrexlemga  10827  leabs  10878  absrele  10887  nn0abscl  10889  ltabs  10891  abslt  10892  absle  10893  abstri  10908  amgm2  10922  sqr11d  10977  abs00d  10990  maxabsle  11008  maxabslemlub  11011  maxleastlt  11019  maxltsup  11022  2zsupmax  11029  minmax  11033  xrmaxleim  11045  xrmaxiflemlub  11049  xrmaxiflemcom  11050  xrmaxiflemval  11051  xrmaxleastlt  11057  xrmaxltsup  11059  xrmaxaddlem  11061  xrmaxadd  11062  xrminmax  11066  xrmin1inf  11068  xrmin2inf  11069  xrmineqinf  11070  climi  11088  reccn2ap  11114  climge0  11126  climle  11135  climserle  11146  climrecvg1n  11149  fz1f1o  11176  summodclem3  11181  summodclem2a  11182  summodc  11184  fisumss  11193  fsum0diaglem  11241  mptfzshft  11243  fsumrev  11244  fisum0diag2  11248  fsumlessfi  11261  fsumle  11264  fsumlt  11265  isumsplit  11292  isumrpcl  11295  expcnvap0  11303  geosergap  11307  pwm1geoserap1  11309  absgtap  11311  geolim  11312  geolim2  11313  georeclim  11314  geoisumr  11319  geoisum1c  11321  cvgratnnlembern  11324  cvgratnnlemseq  11327  cvgratnnlemsumlt  11329  cvgratnnlemfm  11330  cvgratnnlemrate  11331  cvgratnn  11332  cvgratz  11333  mertenslemub  11335  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  prodmodclem2a  11377  prodmodc  11379  zproddc  11380  efcllemp  11401  ege2le3  11414  eftlcvg  11430  eftlub  11433  efltim  11441  eflegeo  11444  tanaddap  11482  sinbnd  11495  cosbnd  11496  sin01bnd  11500  cos01bnd  11501  sin01gt0  11504  cos01gt0  11505  cos12dec  11510  eirraplem  11519  zdvdsdc  11550  dvdstr  11566  dvdsadd2b  11576  dvdslelemd  11577  divconjdvds  11583  alzdvds  11588  dvdsext  11589  fzm1ndvds  11590  fzo0dvdseq  11591  zeo3  11601  even2n  11607  mod2eq1n2dvds  11612  nn0ehalf  11636  nnehalf  11637  nno  11639  nn0oddm1d2  11642  divalglemnqt  11653  divalglemex  11655  divalglemeuneg  11656  divalg2  11659  divalgmod  11660  flodddiv4t2lthalf  11670  zsupcllemstep  11674  infssuzex  11678  dvdsbnd  11681  gcdsupex  11682  gcdsupcl  11683  gcddvds  11688  divgcdz  11696  divgcdnn  11699  gcd0id  11703  gcdneg  11706  gcd1  11711  dvdsgcdidd  11718  bezoutlemnewy  11720  bezoutlemstep  11721  bezoutlemmo  11730  bezoutlemsup  11733  dfgcd3  11734  bezout  11735  dfgcd2  11738  mulgcd  11740  sqgcd  11753  dvdssqlem  11754  bezoutr1  11757  lcmval  11780  lcmcllem  11784  dvdslcm  11786  lcmgcdlem  11794  lcmdvds  11796  lcmgcdeq  11800  ncoprmgcdne1b  11806  mulgcddvds  11811  rpmulgcd2  11812  qredeu  11814  rpdvds  11816  prmind2  11837  nprm  11840  dvdsnprmd  11842  divgcdodd  11857  isprm6  11861  prmexpb  11865  pw2dvds  11880  pw2dvdseulemle  11881  oddpwdclemdc  11887  sqne2sq  11891  znege1  11892  sqrt2irraplemnn  11893  divnumden  11910  divdenle  11911  qden1elz  11919  nn0sqrtelqelz  11920  hashdvds  11933  crth  11936  phimullem  11937  hashgcdlem  11939  oddennn  11941  ennnfonelemk  11949  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemex  11963  ennnfonelemhom  11964  ennnfonelemrnh  11965  ennnfonelemen  11970  ennnfonelemim  11973  ctinfomlemom  11976  ctiunctlemf  11987  ntridm  12334  ntrtop  12336  ntrcls0  12339  ntr0  12342  isopn3i  12343  neiss2  12350  opnneiss  12366  topssnei  12370  cnpf2  12415  icnpimaex  12419  lmcvg  12425  iscnp4  12426  cncnp  12438  cnptopresti  12446  lmfss  12452  lmtopcnp  12458  hmeores  12523  bldisj  12609  xblss2ps  12612  xblss2  12613  blhalf  12616  blssps  12635  blss  12636  ssblex  12639  blpnfctr  12647  xmetresbl  12648  mopni2  12691  bdxmet  12709  bdbl  12711  xmetxpbl  12716  metcnpi  12723  metcnpi2  12724  tgioo  12754  rescncf  12776  mulcncflem  12798  cnopnap  12802  dedekindeulemuub  12803  dedekindeulemloc  12805  dedekindeulemlu  12807  dedekindeu  12809  dedekindicclemuub  12812  dedekindicclemloc  12814  dedekindicclemlu  12816  dedekindicclemicc  12818  dedekindicc  12819  ivthinclemlopn  12822  ivthinclemuopn  12824  ivthdec  12830  limcimolemlt  12841  cnplimcim  12844  cnplimclemr  12846  limccnpcntop  12852  limccnp2cntop  12854  limccoap  12855  dvfgg  12865  dvidlemap  12868  dvaddxxbr  12873  dvmulxxbr  12874  dvaddxx  12875  dvmulxx  12876  dviaddf  12877  dvimulf  12878  dvcoapbr  12879  dvcjbr  12880  dvcj  12881  dvrecap  12885  dvmptclx  12888  dveflem  12895  reeff1oleme  12901  eflt  12904  sin0pilem1  12910  pilem3  12912  cosq14gt0  12961  coseq0negpitopi  12965  tangtx  12967  coskpi  12977  cosordlem  12978  cosq34lt1  12979  relogef  12993  logrpap0d  13007  rplogcl  13008  logge0  13009  logdivlti  13010  cxplt3  13048  rpabscxpbnd  13067  pwf1oexmid  13367  subctctexmid  13369  pw1nct  13371  nnsf  13374  peano4nninf  13375  nninfalllemn  13377  nninfsellemeq  13385  cvgcmp2nlemabs  13402  trilpolemisumle  13406  trilpolemeq1  13408  trilpolemlt1  13409  trirec0  13412  apdifflemf  13414  apdifflemr  13415  apdiff  13416  iswomninnlem  13417  redcwlpo  13422  neapmkvlem  13424  iooref1o  13426  supfz  13428  inffz  13429