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  3327  elinel2  3391  rabsnt  3741  eldifsni  3797  unimax  3922  ssintub  3941  exmidsssnc  4287  moop2  4338  wepo  4450  wetrep  4451  trssord  4471  ordelord  4472  ordsucim  4592  ordtri2or2exmidlem  4618  regexmidlem1  4625  reg2exmidlema  4626  tfis  4675  opelxp2  4754  funmo  5333  funopg  5352  funco  5358  funun  5362  fununi  5389  funimaexglem  5404  fndm  5420  frn  5482  f1ss  5539  f1ssr  5540  f1ssres  5542  forn  5553  f1f1orn  5585  f1orescnv  5590  f1imacnv  5591  funcocnv2  5599  funfveu  5642  nfvres  5665  isorel  5938  isoini2  5949  f1ofveu  5995  fovcld  6115  f1opw  6219  f1o2ndf1  6380  mpoxopn0yelv  6391  swoer  6716  mapsnconst  6849  en0  6955  en1  6959  phplem4  7024  phplem4dom  7031  phplem4on  7037  ssfilem  7045  diffitest  7057  inffiexmid  7076  supubti  7174  suplubti  7175  djuinr  7238  casefun  7260  casef1  7265  djufun  7279  nnnninfeq  7303  ctssexmid  7325  exmidonfinlem  7379  exmidfodomrlemim  7387  cc4f  7463  cc4n  7465  0npi  7508  mulclpi  7523  mulcanpig  7530  nlt1pig  7536  indpi  7537  nnppipi  7538  dfplpq2  7549  archnqq  7612  enq0tr  7629  nqnq0pi  7633  ltexprlemopl  7796  ltexprlemopu  7798  cauappcvgprlemopl  7841  cauappcvgprlemlol  7842  cauappcvgprlemopu  7843  cauappcvgprlemupu  7844  cauappcvgprlemdisj  7846  caucvgprlemopl  7864  caucvgprlemlol  7865  caucvgprlemopu  7866  caucvgprlemupu  7867  caucvgprlemdisj  7869  caucvgprprlemopl  7892  caucvgprprlemlol  7893  caucvgprprlemopu  7894  caucvgprprlemupu  7895  caucvgprprlemdisj  7897  suplocsrlempr  8002  ltresr2  8035  peano2nnnn  8048  axrnegex  8074  ltxrlt  8220  peano2nn  9130  elnn0z  9467  zaddcl  9494  ztri3or0  9496  eluz2gt1  9805  1nuz2  9809  rpgt0  9869  ixxss1  10108  ixxss2  10109  ixxss12  10110  iccss2  10148  iccssico2  10151  elfzuz3  10226  uzdisj  10297  nn0disj  10342  zsupcllemstep  10457  zsupssdc  10466  addmodlteq  10628  expge0  10805  expge1  10806  expaddzaplem  10812  shftfn  11343  fsumf1o  11909  fsumge0  11978  fprodf1o  12107  bitsfzolem  12473  bezoutlemzz  12531  bezoutlemaz  12532  bezoutlembz  12533  bezoutlemsup  12538  1nprm  12644  nprm  12653  sqnprm  12666  dvdsprm  12667  coprm  12674  sqpweven  12705  2sqpwodd  12706  dfphi2  12750  phimullem  12755  eulerthlemrprm  12759  phisum  12771  expnprm  12884  1arith  12898  4sqlem18  12939  oddennn  12971  znnen  12977  ennnfonelemg  12982  ctinf  13009  mndid  13466  mhmf  13506  mhmlin  13508  mhm0  13509  grpinvex  13551  grplinv  13591  mulgz  13695  mulgdirlem  13698  mulgdir  13699  mulgass  13704  nsgbi  13749  nmzbi  13754  ghmf  13792  ghmlin  13793  conjnsg  13826  ablcmn  13836  cmncom  13847  crngmgp  13975  rhmmhm  14131  rhmghm  14134  rimf1o  14142  nzrnz  14154  subrgss  14194  subrg1cl  14201  rrgeq0i  14236  domneq0  14244  2idlelbas  14488  2idlcpblrng  14495  znidomb  14630  toponuni  14697  tpsuni  14716  neipsm  14836  cnf  14886  cnima  14902  txdis1cn  14960  hmeocnvcn  14988  psmetxrge0  15014  isxmet2d  15030  xmstopn  15137  mstopn  15138  bdxmet  15183  divcnap  15247  ivthinclemlr  15319  ivthinclemur  15321  dvlemap  15362  dvcnp2cntop  15381  dvaddxxbr  15383  dvmulxxbr  15384  dvcoapbr  15389  dvcjbr  15390  dvrecap  15395  dveflem  15408  plyf  15419  plyadd  15433  plymul  15434  plycn  15444  dvply2g  15448  dvdsppwf1o  15671  mpodvdsmulf1o  15672  lgsfle1  15696  lgsle1  15702  lgsdirprm  15721  lgsne0  15725  lgsquadlem1  15764  lgsquadlem2  15765  upgr1or2  15909  umgredg2en  15917  lfgredg2dom  15938  upgr2wlkdc  16096  trlres  16108  bj-indsuc  16315  nnsf  16401