Theorem simprbi 275

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simprbi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simprbi	⊢ (𝜑 → 𝜒)

Proof of Theorem simprbi

Step	Hyp	Ref	Expression
1		simprbi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	biimpi 120	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 114	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.63dc  952  sb1  1812  reurmo  2751  eldifn  3328  elinel2  3392  rabsnt  3744  eldifsni  3800  unimax  3925  ssintub  3944  exmidsssnc  4291  moop2  4342  wepo  4454  wetrep  4455  trssord  4475  ordelord  4476  ordsucim  4596  ordtri2or2exmidlem  4622  regexmidlem1  4629  reg2exmidlema  4630  tfis  4679  opelxp2  4758  funmo  5339  funopg  5358  funco  5364  funun  5368  fununi  5395  funimaexglem  5410  fndm  5426  frn  5488  f1ss  5545  f1ssr  5546  f1ssres  5548  forn  5559  f1f1orn  5591  f1orescnv  5596  f1imacnv  5597  funcocnv2  5605  funfveu  5648  nfvres  5671  isorel  5944  isoini2  5955  f1ofveu  6001  fovcld  6121  f1opw  6225  f1o2ndf1  6388  mpoxopn0yelv  6400  swoer  6725  mapsnconst  6858  en0  6964  en1  6968  phplem4  7036  phplem4dom  7043  phplem4on  7049  ssfilem  7057  ssfilemd  7059  diffitest  7071  inffiexmid  7093  supubti  7192  suplubti  7193  djuinr  7256  casefun  7278  casef1  7283  djufun  7297  nnnninfeq  7321  ctssexmid  7343  exmidonfinlem  7397  exmidfodomrlemim  7405  cc4f  7481  cc4n  7483  0npi  7526  mulclpi  7541  mulcanpig  7548  nlt1pig  7554  indpi  7555  nnppipi  7556  dfplpq2  7567  archnqq  7630  enq0tr  7647  nqnq0pi  7651  ltexprlemopl  7814  ltexprlemopu  7816  cauappcvgprlemopl  7859  cauappcvgprlemlol  7860  cauappcvgprlemopu  7861  cauappcvgprlemupu  7862  cauappcvgprlemdisj  7864  caucvgprlemopl  7882  caucvgprlemlol  7883  caucvgprlemopu  7884  caucvgprlemupu  7885  caucvgprlemdisj  7887  caucvgprprlemopl  7910  caucvgprprlemlol  7911  caucvgprprlemopu  7912  caucvgprprlemupu  7913  caucvgprprlemdisj  7915  suplocsrlempr  8020  ltresr2  8053  peano2nnnn  8066  axrnegex  8092  ltxrlt  8238  peano2nn  9148  elnn0z  9485  zaddcl  9512  ztri3or0  9514  eluz2gt1  9829  1nuz2  9833  rpgt0  9893  ixxss1  10132  ixxss2  10133  ixxss12  10134  iccss2  10172  iccssico2  10175  elfzuz3  10250  uzdisj  10321  nn0disj  10366  zsupcllemstep  10482  zsupssdc  10491  addmodlteq  10653  expge0  10830  expge1  10831  expaddzaplem  10837  shftfn  11378  fsumf1o  11944  fsumge0  12013  fprodf1o  12142  bitsfzolem  12508  bezoutlemzz  12566  bezoutlemaz  12567  bezoutlembz  12568  bezoutlemsup  12573  1nprm  12679  nprm  12688  sqnprm  12701  dvdsprm  12702  coprm  12709  sqpweven  12740  2sqpwodd  12741  dfphi2  12785  phimullem  12790  eulerthlemrprm  12794  phisum  12806  expnprm  12919  1arith  12933  4sqlem18  12974  oddennn  13006  znnen  13012  ennnfonelemg  13017  ctinf  13044  mndid  13501  mhmf  13541  mhmlin  13543  mhm0  13544  grpinvex  13586  grplinv  13626  mulgz  13730  mulgdirlem  13733  mulgdir  13734  mulgass  13739  nsgbi  13784  nmzbi  13789  ghmf  13827  ghmlin  13828  conjnsg  13861  ablcmn  13871  cmncom  13882  crngmgp  14010  rhmmhm  14166  rhmghm  14169  rimf1o  14177  nzrnz  14189  subrgss  14229  subrg1cl  14236  rrgeq0i  14271  domneq0  14279  2idlelbas  14523  2idlcpblrng  14530  znidomb  14665  toponuni  14732  tpsuni  14751  neipsm  14871  cnf  14921  cnima  14937  txdis1cn  14995  hmeocnvcn  15023  psmetxrge0  15049  isxmet2d  15065  xmstopn  15172  mstopn  15173  bdxmet  15218  divcnap  15282  ivthinclemlr  15354  ivthinclemur  15356  dvlemap  15397  dvcnp2cntop  15416  dvaddxxbr  15418  dvmulxxbr  15419  dvcoapbr  15424  dvcjbr  15425  dvrecap  15430  dveflem  15443  plyf  15454  plyadd  15468  plymul  15469  plycn  15479  dvply2g  15483  dvdsppwf1o  15706  mpodvdsmulf1o  15707  lgsfle1  15731  lgsle1  15737  lgsdirprm  15756  lgsne0  15760  lgsquadlem1  15799  lgsquadlem2  15800  upgr1or2  15945  umgredg2en  15953  lfgredg2dom  15976  upgr2wlkdc  16186  trlres  16199  clwwlknon  16238  bj-indsuc  16473  nnsf  16557