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  948  sb1  1780  reurmo  2716  eldifn  3287  elinel2  3351  rabsnt  3698  eldifsni  3752  unimax  3874  ssintub  3893  exmidsssnc  4237  moop2  4285  wepo  4395  wetrep  4396  trssord  4416  ordelord  4417  ordsucim  4537  ordtri2or2exmidlem  4563  regexmidlem1  4570  reg2exmidlema  4571  tfis  4620  opelxp2  4699  funmo  5274  funopg  5293  funco  5299  funun  5303  fununi  5327  funimaexglem  5342  fndm  5358  frn  5419  f1ss  5472  f1ssr  5473  f1ssres  5475  forn  5486  f1f1orn  5518  f1orescnv  5523  f1imacnv  5524  funcocnv2  5532  funfveu  5574  nfvres  5595  isorel  5858  isoini2  5869  f1ofveu  5913  fovcld  6031  f1opw  6134  f1o2ndf1  6295  mpoxopn0yelv  6306  swoer  6629  mapsnconst  6762  en0  6863  en1  6867  phplem4  6925  phplem4dom  6932  phplem4on  6937  ssfilem  6945  diffitest  6957  inffiexmid  6976  supubti  7074  suplubti  7075  djuinr  7138  casefun  7160  casef1  7165  djufun  7179  nnnninfeq  7203  ctssexmid  7225  exmidonfinlem  7274  exmidfodomrlemim  7282  cc4f  7354  cc4n  7356  0npi  7399  mulclpi  7414  mulcanpig  7421  nlt1pig  7427  indpi  7428  nnppipi  7429  dfplpq2  7440  archnqq  7503  enq0tr  7520  nqnq0pi  7524  ltexprlemopl  7687  ltexprlemopu  7689  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemopu  7734  cauappcvgprlemupu  7735  cauappcvgprlemdisj  7737  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemopu  7757  caucvgprlemupu  7758  caucvgprlemdisj  7760  caucvgprprlemopl  7783  caucvgprprlemlol  7784  caucvgprprlemopu  7785  caucvgprprlemupu  7786  caucvgprprlemdisj  7788  suplocsrlempr  7893  ltresr2  7926  peano2nnnn  7939  axrnegex  7965  ltxrlt  8111  peano2nn  9021  elnn0z  9358  zaddcl  9385  ztri3or0  9387  eluz2gt1  9695  1nuz2  9699  rpgt0  9759  ixxss1  9998  ixxss2  9999  ixxss12  10000  iccss2  10038  iccssico2  10041  elfzuz3  10116  uzdisj  10187  nn0disj  10232  zsupcllemstep  10338  zsupssdc  10347  addmodlteq  10509  expge0  10686  expge1  10687  expaddzaplem  10693  shftfn  11008  fsumf1o  11574  fsumge0  11643  fprodf1o  11772  bitsfzolem  12138  bezoutlemzz  12196  bezoutlemaz  12197  bezoutlembz  12198  bezoutlemsup  12203  1nprm  12309  nprm  12318  sqnprm  12331  dvdsprm  12332  coprm  12339  sqpweven  12370  2sqpwodd  12371  dfphi2  12415  phimullem  12420  eulerthlemrprm  12424  phisum  12436  expnprm  12549  1arith  12563  4sqlem18  12604  oddennn  12636  znnen  12642  ennnfonelemg  12647  ctinf  12674  mndid  13129  mhmf  13169  mhmlin  13171  mhm0  13172  grpinvex  13214  grplinv  13254  mulgz  13358  mulgdirlem  13361  mulgdir  13362  mulgass  13367  nsgbi  13412  nmzbi  13417  ghmf  13455  ghmlin  13456  conjnsg  13489  ablcmn  13499  cmncom  13510  crngmgp  13638  rhmmhm  13793  rhmghm  13796  rimf1o  13804  nzrnz  13816  subrgss  13856  subrg1cl  13863  rrgeq0i  13898  domneq0  13906  2idlelbas  14150  2idlcpblrng  14157  znidomb  14292  toponuni  14337  tpsuni  14356  neipsm  14476  cnf  14526  cnima  14542  txdis1cn  14600  hmeocnvcn  14628  psmetxrge0  14654  isxmet2d  14670  xmstopn  14777  mstopn  14778  bdxmet  14823  divcnap  14887  ivthinclemlr  14959  ivthinclemur  14961  dvlemap  15002  dvcnp2cntop  15021  dvaddxxbr  15023  dvmulxxbr  15024  dvcoapbr  15029  dvcjbr  15030  dvrecap  15035  dveflem  15048  plyf  15059  plyadd  15073  plymul  15074  plycn  15084  dvply2g  15088  dvdsppwf1o  15311  mpodvdsmulf1o  15312  lgsfle1  15336  lgsle1  15342  lgsdirprm  15361  lgsne0  15365  lgsquadlem1  15404  lgsquadlem2  15405  bj-indsuc  15660  nnsf  15738