Theorem mpbird 165

Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpbird.min	⊢ (𝜑 → 𝜒)
mpbird.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbird	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbird

Step	Hyp	Ref	Expression
1		mpbird.min	. 2 ⊢ (𝜑 → 𝜒)
2		mpbird.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimprd 156	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpbiri  166  pm5.19  654  mpbir2and  885  pm3.12dc  899  mpbir3and  1121  pm5.15dc  1320  eqeltrd  2155  eqnetrd  2269  3netr4d  2278  sbcne12g  2924  eqsstrd  3033  3sstr4d  3042  eqbrtrd  3805  3brtr4d  3815  snelpwi  3967  prelpwi  3969  pwel  3973  ordelon  4138  onin  4141  elelsuc  4164  suceloni  4245  sucelon  4247  onintonm  4261  sosng  4431  relssdv  4450  eqbrrdv  4455  eqrelrdv2  4457  breldmg  4559  iss  4674  xpimasn  4789  elxp4  4828  elxp5  4829  funssres  4962  sefvex  5216  fvun1  5260  eqfnfvd  5289  fvimacnvi  5302  fvimacnv  5303  fvelrn  5319  fmpt2d  5348  fmptco  5351  fsn  5356  ftpg  5368  fconst2g  5397  funfvima3  5413  foeqcnvco  5450  f1eqcocnv  5451  fliftfun  5456  fliftfund  5457  fliftval  5460  riota5f  5512  f1ofveu  5520  f1ocnvd  5722  f1opw2  5726  fnofval  5741  off  5744  offval2  5746  ofrfval2  5747  caofref  5752  caofinvl  5753  elxp6  5816  cnvf1olem  5865  f2ndf  5867  f1od2  5876  tposf12  5907  smores2  5932  tfrlemisucaccv  5962  tfrlemibfn  5965  tfri3  5976  frecsuclemdm  6011  nnsucsssuc  6094  ersym  6141  ertr  6144  swoer  6157  erth  6173  riinerm  6202  qliftfund  6212  eroprf  6222  ecopoverg  6230  th3qlem1  6231  f1dom2g  6259  dom3d  6277  fopwdom  6333  nndomo  6350  dif1en  6364  findcard2  6373  findcard2s  6374  diffisn  6377  fientri3  6381  f1dmvrnfibi  6393  supelti  6415  supsnti  6418  cnvinfex  6431  ordiso2  6446  isnumi  6451  ltsopi  6510  pitri3or  6512  ltdcpi  6513  indpi  6532  enqdc  6551  enqdc1  6552  addcmpblnq  6557  mulcanenq  6575  recrecnq  6584  nqtri3or  6586  ltdcnq  6587  ltsonq  6588  ltaddnq  6597  subhalfnqq  6604  archnqq  6607  prarloclemarch2  6609  enq0tr  6624  nqnq0  6631  addcmpblnq0  6633  mulcanenq0ec  6635  nnnq0lem1  6636  nqpnq0nq  6643  nq0m0r  6646  nq02m  6655  prarloclemlt  6683  prarloclemcalc  6692  addlocpr  6726  nqprl  6741  nqpru  6742  addnqprlemrl  6747  addnqprlemru  6748  prmuloclemcalc  6755  mullocprlem  6760  mulnqprlemrl  6763  mulnqprlemru  6764  1idprl  6780  1idpru  6781  ltaddpr  6787  ltexprlemm  6790  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemdisj  6796  ltexprlemrl  6800  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  addcanprg  6806  prplnqu  6810  recexprlemloc  6821  recexprlem1ssl  6823  recexprlem1ssu  6824  aptiprleml  6829  aptiprlemu  6830  archpr  6833  cauappcvgprlemm  6835  cauappcvgprlemopl  6836  cauappcvgprlemloc  6842  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlem1  6849  cauappcvgprlem2  6850  caucvgprlemnkj  6856  caucvgprlemopl  6859  caucvgprlemloc  6865  caucvgprlemladdfu  6867  caucvgprlem2  6870  caucvgprprlemnkltj  6879  caucvgprprlemopl  6887  caucvgprprlemloc  6893  caucvgprprlemexbt  6896  caucvgprprlemaddq  6898  caucvgprprlem2  6900  prsrlem1  6919  0idsr  6944  1idsr  6945  recexgt0sr  6950  archsr  6958  prsradd  6962  caucvgsrlemcau  6969  caucvgsrlembound  6970  caucvgsrlemoffgt1  6975  pitonnlem1p1  7014  pitonn  7016  pitoregt0  7017  peano2nnnn  7021  recidpirq  7026  axcaucvglemval  7063  leid  7195  nltled  7230  readdcan  7248  addneintrd  7296  addneintr2d  7297  pncan  7314  subsub2  7336  subsub4  7341  negned  7416  subne0d  7428  subneintrd  7463  subneintr2d  7465  subeq0bd  7483  subdi  7489  gt0add  7673  rimul  7685  rereim  7686  ltmul1a  7691  apreim  7703  apirr  7705  mulap0r  7715  msqge0  7716  mulge0  7719  gt0ap0  7725  ltap  7731  recexaplem2  7742  mulap0bad  7749  mulap0bbd  7750  divrecap  7776  div0ap  7790  div1  7791  recrecap  7797  divdivdivap  7801  ddcanap  7814  rerecclap  7818  div2negap  7823  recgt0  7928  prodgt0  7930  lemul1a  7936  recp1lt1  7977  squeeze0  7982  peano2nn  8051  div4p1lem1div2  8284  arch  8285  peano2z  8387  peano2zm  8389  ztri3or  8394  nn0n0n1ge2  8418  zextle  8438  gtndiv  8442  suprzclex  8445  nn0ind-raph  8464  uzid  8633  uzneg  8637  uztric  8640  uz11  8641  eluzp1l  8643  qdivcl  8728  irrmul  8732  rpnegap  8766  ledivge1le  8803  nn0ledivnn  8838  ltpnf  8856  mnflt  8858  pnfge  8864  mnfle  8867  xrlttr  8870  xrltso  8871  xrlttri3  8872  xrleid  8874  iccf1o  9026  fztri3or  9058  fznlem  9060  fzn  9061  fzsplit2  9069  fznatpl1  9093  uzsplit  9109  fseq1p1m1  9111  fzm1  9117  fznn0sub2  9139  difelfznle  9146  1fv  9149  fzospliti  9185  fzouzsplit  9188  eluzgtdifelfzo  9206  exfzdc  9249  subfzo0  9251  qbtwnz  9260  qbtwnrelemcalc  9264  flqlelt  9278  qfraclt1  9282  qfracge0  9283  flqltnz  9289  btwnzge0  9302  flhalf  9304  ceiqle  9315  intfracq  9322  mulqmod0  9332  modqge0  9334  modqlt  9335  modqid  9351  modqid0  9352  m1modge3gt1  9373  modqltm1p1mod  9378  q2txmodxeq0  9386  modaddmodlo  9390  modsumfzodifsn  9398  addmodlteq  9400  frecuzrdgfn  9414  uzsinds  9428  monoord2  9456  iseqid3  9465  serile  9474  expivallem  9477  expival  9478  expp1  9483  expcllem  9487  ltexp2a  9528  leexp2a  9529  faclbnd  9668  faclbnd2  9669  faclbnd3  9670  ibcval5  9690  bcpasc  9693  shftfn  9712  cjth  9733  cjmulrcl  9774  reim0bd  9831  rerebd  9832  cjrebd  9833  caucvgre  9867  cvg1nlemcxze  9868  cvg1nlemcau  9870  cvg1nlemres  9871  recvguniq  9881  resqrexlemover  9896  resqrexlemdec  9897  resqrexlemgt0  9906  resqrexlemoverl  9907  resqrexlemglsq  9908  rersqrtthlem  9916  sqrtgt0  9920  leabs  9960  absexpzap  9966  absle  9975  recvalap  9983  abstri  9990  abs2dif  9992  amgm2  10004  absne0d  10073  maxleim  10091  maxabslemab  10092  maxabslemlub  10093  maxltsup  10104  fimaxre2  10109  minmax  10112  climconst  10129  climuni  10132  2clim  10140  climcn1  10147  climcn2  10148  climge0  10163  climle  10172  climsqz  10173  climsqz2  10174  serif0  10189  dvdsval2  10198  dvdsdc  10203  dvds0lem  10205  zdvdsdc  10216  dvdscmulr  10224  dvdsmulcr  10225  dvdslelemd  10243  divconjdvds  10249  dvdsext  10255  fzm1ndvds  10256  dvdsmod  10262  oexpneg  10276  2tp1odd  10284  mulsucdiv2z  10285  2teven  10287  zeo5  10288  opeo  10297  omeo  10298  nn0ob  10308  divalglemnqt  10320  zsupcllemstep  10341  zsupcl  10343  zssinfcl  10344  infssuzex  10345  infssuzcldc  10347  gcddvds  10355  dvdslegcd  10356  gcdneg  10373  bezoutlemnewy  10385  bezoutlemstep  10386  bezoutlema  10388  bezoutlemb  10389  bezoutlemmo  10395  bezoutlemle  10397  bezoutlemsup  10398  dfgcd3  10399  bezout  10400  dfgcd2  10403  lcmcllem  10449  lcmneg  10456  lcmgcdlem  10459  lcmdvds  10461  lcmid  10462  3lcm2e6woprm  10468  6lcm4e12  10469  ncoprmgcdne1b  10471  mulgcddvds  10476  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  isprm2lem  10498  prmind2  10502  dvdsnprmd  10507  prm2orodd  10508  sqnprm  10517  rpexp  10532  sqrt2irrlem  10540  oddpwdclemdc  10551  sqrt2irraplemnn  10557  bj-sels  10705  bj-nnelon  10754