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  949  sb1  1790  reurmo  2726  eldifn  3297  elinel2  3361  rabsnt  3709  eldifsni  3764  unimax  3886  ssintub  3905  exmidsssnc  4251  moop2  4300  wepo  4410  wetrep  4411  trssord  4431  ordelord  4432  ordsucim  4552  ordtri2or2exmidlem  4578  regexmidlem1  4585  reg2exmidlema  4586  tfis  4635  opelxp2  4714  funmo  5291  funopg  5310  funco  5316  funun  5320  fununi  5347  funimaexglem  5362  fndm  5378  frn  5440  f1ss  5494  f1ssr  5495  f1ssres  5497  forn  5508  f1f1orn  5540  f1orescnv  5545  f1imacnv  5546  funcocnv2  5554  funfveu  5596  nfvres  5617  isorel  5884  isoini2  5895  f1ofveu  5939  fovcld  6057  f1opw  6160  f1o2ndf1  6321  mpoxopn0yelv  6332  swoer  6655  mapsnconst  6788  en0  6894  en1  6898  phplem4  6959  phplem4dom  6966  phplem4on  6971  ssfilem  6979  diffitest  6991  inffiexmid  7010  supubti  7108  suplubti  7109  djuinr  7172  casefun  7194  casef1  7199  djufun  7213  nnnninfeq  7237  ctssexmid  7259  exmidonfinlem  7308  exmidfodomrlemim  7316  cc4f  7388  cc4n  7390  0npi  7433  mulclpi  7448  mulcanpig  7455  nlt1pig  7461  indpi  7462  nnppipi  7463  dfplpq2  7474  archnqq  7537  enq0tr  7554  nqnq0pi  7558  ltexprlemopl  7721  ltexprlemopu  7723  cauappcvgprlemopl  7766  cauappcvgprlemlol  7767  cauappcvgprlemopu  7768  cauappcvgprlemupu  7769  cauappcvgprlemdisj  7771  caucvgprlemopl  7789  caucvgprlemlol  7790  caucvgprlemopu  7791  caucvgprlemupu  7792  caucvgprlemdisj  7794  caucvgprprlemopl  7817  caucvgprprlemlol  7818  caucvgprprlemopu  7819  caucvgprprlemupu  7820  caucvgprprlemdisj  7822  suplocsrlempr  7927  ltresr2  7960  peano2nnnn  7973  axrnegex  7999  ltxrlt  8145  peano2nn  9055  elnn0z  9392  zaddcl  9419  ztri3or0  9421  eluz2gt1  9730  1nuz2  9734  rpgt0  9794  ixxss1  10033  ixxss2  10034  ixxss12  10035  iccss2  10073  iccssico2  10076  elfzuz3  10151  uzdisj  10222  nn0disj  10267  zsupcllemstep  10379  zsupssdc  10388  addmodlteq  10550  expge0  10727  expge1  10728  expaddzaplem  10734  shftfn  11179  fsumf1o  11745  fsumge0  11814  fprodf1o  11943  bitsfzolem  12309  bezoutlemzz  12367  bezoutlemaz  12368  bezoutlembz  12369  bezoutlemsup  12374  1nprm  12480  nprm  12489  sqnprm  12502  dvdsprm  12503  coprm  12510  sqpweven  12541  2sqpwodd  12542  dfphi2  12586  phimullem  12591  eulerthlemrprm  12595  phisum  12607  expnprm  12720  1arith  12734  4sqlem18  12775  oddennn  12807  znnen  12813  ennnfonelemg  12818  ctinf  12845  mndid  13301  mhmf  13341  mhmlin  13343  mhm0  13344  grpinvex  13386  grplinv  13426  mulgz  13530  mulgdirlem  13533  mulgdir  13534  mulgass  13539  nsgbi  13584  nmzbi  13589  ghmf  13627  ghmlin  13628  conjnsg  13661  ablcmn  13671  cmncom  13682  crngmgp  13810  rhmmhm  13965  rhmghm  13968  rimf1o  13976  nzrnz  13988  subrgss  14028  subrg1cl  14035  rrgeq0i  14070  domneq0  14078  2idlelbas  14322  2idlcpblrng  14329  znidomb  14464  toponuni  14531  tpsuni  14550  neipsm  14670  cnf  14720  cnima  14736  txdis1cn  14794  hmeocnvcn  14822  psmetxrge0  14848  isxmet2d  14864  xmstopn  14971  mstopn  14972  bdxmet  15017  divcnap  15081  ivthinclemlr  15153  ivthinclemur  15155  dvlemap  15196  dvcnp2cntop  15215  dvaddxxbr  15217  dvmulxxbr  15218  dvcoapbr  15223  dvcjbr  15224  dvrecap  15229  dveflem  15242  plyf  15253  plyadd  15267  plymul  15268  plycn  15278  dvply2g  15282  dvdsppwf1o  15505  mpodvdsmulf1o  15506  lgsfle1  15530  lgsle1  15536  lgsdirprm  15555  lgsne0  15559  lgsquadlem1  15598  lgsquadlem2  15599  bj-indsuc  15938  nnsf  16016