Theorem simprbi 273

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 119	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 113	1 ⊢ (𝜑 → 𝜒)

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.63dc  931  sb1  1740  reurmo  2648  eldifn  3204  elinel2  3268  rabsnt  3606  eldifsni  3660  unimax  3778  ssintub  3797  exmidsssnc  4134  moop2  4181  wepo  4289  wetrep  4290  trssord  4310  ordelord  4311  ordsucim  4424  ordtri2or2exmidlem  4449  regexmidlem1  4456  reg2exmidlema  4457  tfis  4505  opelxp2  4582  funmo  5146  funopg  5165  funco  5171  funun  5175  fununi  5199  funimaexglem  5214  fndm  5230  frn  5289  f1ss  5342  f1ssr  5343  f1ssres  5345  forn  5356  f1f1orn  5386  f1orescnv  5391  f1imacnv  5392  funcocnv2  5400  funfveu  5442  nfvres  5462  isorel  5717  isoini2  5728  f1ofveu  5770  fovcl  5884  f1opw  5985  f1o2ndf1  6133  mpoxopn0yelv  6144  swoer  6465  mapsnconst  6596  en0  6697  en1  6701  phplem4  6757  phplem4dom  6764  phplem4on  6769  ssfilem  6777  diffitest  6789  inffiexmid  6808  supubti  6894  suplubti  6895  djuinr  6956  casefun  6978  casef1  6983  djufun  6997  ctssexmid  7032  exmidonfinlem  7066  exmidfodomrlemim  7074  cc4f  7101  cc4n  7103  0npi  7145  mulclpi  7160  mulcanpig  7167  nlt1pig  7173  indpi  7174  nnppipi  7175  dfplpq2  7186  archnqq  7249  enq0tr  7266  nqnq0pi  7270  ltexprlemopl  7433  ltexprlemopu  7435  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemopu  7480  cauappcvgprlemupu  7481  cauappcvgprlemdisj  7483  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemopu  7503  caucvgprlemupu  7504  caucvgprlemdisj  7506  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemopu  7531  caucvgprprlemupu  7532  caucvgprprlemdisj  7534  suplocsrlempr  7639  ltresr2  7672  peano2nnnn  7685  axrnegex  7711  ltxrlt  7854  peano2nn  8756  elnn0z  9091  zaddcl  9118  ztri3or0  9120  eluz2gt1  9423  1nuz2  9427  rpgt0  9482  ixxss1  9717  ixxss2  9718  ixxss12  9719  iccss2  9757  iccssico2  9760  elfzuz3  9834  uzdisj  9904  nn0disj  9946  addmodlteq  10202  expge0  10360  expge1  10361  expaddzaplem  10367  shftfn  10628  fsumf1o  11191  fsumge0  11260  zsupcllemstep  11674  bezoutlemzz  11726  bezoutlemaz  11727  bezoutlembz  11728  bezoutlemsup  11733  1nprm  11831  nprm  11840  sqnprm  11852  dvdsprm  11853  coprm  11858  sqpweven  11889  2sqpwodd  11890  dfphi2  11932  phimullem  11937  oddennn  11941  znnen  11947  ennnfonelemg  11952  ctinf  11979  toponuni  12221  tpsuni  12240  neipsm  12362  cnf  12412  cnima  12428  txdis1cn  12486  hmeocnvcn  12514  psmetxrge0  12540  isxmet2d  12556  xmstopn  12663  mstopn  12664  bdxmet  12709  divcnap  12763  ivthinclemlr  12823  ivthinclemur  12825  dvlemap  12857  dvcnp2cntop  12871  dvaddxxbr  12873  dvmulxxbr  12874  dvcoapbr  12879  dvcjbr  12880  dvrecap  12885  dveflem  12895  bj-indsuc  13297  nnsf  13374  nninfalllemn  13377