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  930  sb1  1739  reurmo  2643  eldifn  3194  elinel2  3258  rabsnt  3593  eldifsni  3647  unimax  3765  ssintub  3784  exmidsssnc  4121  moop2  4168  wepo  4276  wetrep  4277  trssord  4297  ordelord  4298  ordsucim  4411  ordtri2or2exmidlem  4436  regexmidlem1  4443  reg2exmidlema  4444  tfis  4492  opelxp2  4569  funmo  5133  funopg  5152  funco  5158  funun  5162  fununi  5186  funimaexglem  5201  fndm  5217  frn  5276  f1ss  5329  f1ssr  5330  f1ssres  5332  forn  5343  f1f1orn  5371  f1orescnv  5376  f1imacnv  5377  funcocnv2  5385  funfveu  5427  nfvres  5447  isorel  5702  isoini2  5713  f1ofveu  5755  fovcl  5869  f1opw  5970  f1o2ndf1  6118  mpoxopn0yelv  6129  swoer  6450  mapsnconst  6581  en0  6682  en1  6686  phplem4  6742  phplem4dom  6749  phplem4on  6754  ssfilem  6762  diffitest  6774  inffiexmid  6793  supubti  6879  suplubti  6880  djuinr  6941  casefun  6963  casef1  6968  djufun  6982  ctssexmid  7017  exmidonfinlem  7042  exmidfodomrlemim  7050  0npi  7114  mulclpi  7129  mulcanpig  7136  nlt1pig  7142  indpi  7143  nnppipi  7144  dfplpq2  7155  archnqq  7218  enq0tr  7235  nqnq0pi  7239  ltexprlemopl  7402  ltexprlemopu  7404  cauappcvgprlemopl  7447  cauappcvgprlemlol  7448  cauappcvgprlemopu  7449  cauappcvgprlemupu  7450  cauappcvgprlemdisj  7452  caucvgprlemopl  7470  caucvgprlemlol  7471  caucvgprlemopu  7472  caucvgprlemupu  7473  caucvgprlemdisj  7475  caucvgprprlemopl  7498  caucvgprprlemlol  7499  caucvgprprlemopu  7500  caucvgprprlemupu  7501  caucvgprprlemdisj  7503  suplocsrlempr  7608  ltresr2  7641  peano2nnnn  7654  axrnegex  7680  ltxrlt  7823  peano2nn  8725  elnn0z  9060  zaddcl  9087  ztri3or0  9089  eluz2gt1  9389  1nuz2  9393  rpgt0  9446  ixxss1  9680  ixxss2  9681  ixxss12  9682  iccss2  9720  iccssico2  9723  elfzuz3  9796  uzdisj  9866  nn0disj  9908  addmodlteq  10164  expge0  10322  expge1  10323  expaddzaplem  10329  shftfn  10589  fsumf1o  11152  fsumge0  11221  zsupcllemstep  11627  bezoutlemzz  11679  bezoutlemaz  11680  bezoutlembz  11681  bezoutlemsup  11686  1nprm  11784  nprm  11793  sqnprm  11805  dvdsprm  11806  coprm  11811  sqpweven  11842  2sqpwodd  11843  dfphi2  11885  phimullem  11890  oddennn  11894  znnen  11900  ennnfonelemg  11905  ctinf  11932  toponuni  12171  tpsuni  12190  neipsm  12312  cnf  12362  cnima  12378  txdis1cn  12436  hmeocnvcn  12464  psmetxrge0  12490  isxmet2d  12506  xmstopn  12613  mstopn  12614  bdxmet  12659  divcnap  12713  ivthinclemlr  12773  ivthinclemur  12775  dvlemap  12807  dvcnp2cntop  12821  dvaddxxbr  12823  dvmulxxbr  12824  dvcoapbr  12829  dvcjbr  12830  dvrecap  12835  dveflem  12844  bj-indsuc  13115  nnsf  13188  nninfalllemn  13191