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  955  sb1  1815  reurmo  2763  eldifn  3341  elinel2  3405  rabsnt  3765  eldifsni  3821  unimax  3947  ssintub  3966  exmidsssnc  4315  moop2  4367  wepo  4479  wetrep  4480  trssord  4500  ordelord  4501  ordsucim  4621  ordtri2or2exmidlem  4647  regexmidlem1  4654  reg2exmidlema  4655  tfis  4704  opelxp2  4783  funmo  5366  funopg  5385  funco  5391  funun  5396  fununi  5423  funimaexglem  5438  fndm  5454  frn  5516  f1ss  5578  f1ssr  5579  f1ssres  5581  forn  5592  f1f1orn  5624  f1orescnv  5629  f1imacnv  5630  funcocnv2  5638  funfveu  5682  nfvres  5705  isorel  5980  isoini2  5991  f1ofveu  6037  fovcld  6157  f1opw  6261  f1o2ndf1  6423  mpoxopn0yelv  6469  swoer  6794  mapsnconst  6928  en0  7034  en1  7038  phplem4  7108  phplem4dom  7115  phplem4on  7121  ssfilem  7129  ssfilemd  7131  diffitest  7143  inffiexmid  7165  fsuppcorn  7253  supubti  7289  suplubti  7290  djuinr  7353  casefun  7375  casef1  7380  djufun  7394  nnnninfeq  7418  ctssexmid  7440  exmidonfinlem  7495  exmidfodomrlemim  7503  cc4f  7579  cc4n  7581  0npi  7624  mulclpi  7639  mulcanpig  7646  nlt1pig  7652  indpi  7653  nnppipi  7654  dfplpq2  7665  archnqq  7728  enq0tr  7745  nqnq0pi  7749  ltexprlemopl  7912  ltexprlemopu  7914  cauappcvgprlemopl  7957  cauappcvgprlemlol  7958  cauappcvgprlemopu  7959  cauappcvgprlemupu  7960  cauappcvgprlemdisj  7962  caucvgprlemopl  7980  caucvgprlemlol  7981  caucvgprlemopu  7982  caucvgprlemupu  7983  caucvgprlemdisj  7985  caucvgprprlemopl  8008  caucvgprprlemlol  8009  caucvgprprlemopu  8010  caucvgprprlemupu  8011  caucvgprprlemdisj  8013  suplocsrlempr  8118  ltresr2  8151  peano2nnnn  8164  axrnegex  8190  ltxrlt  8335  peano2nn  9245  elnn0z  9586  zaddcl  9613  ztri3or0  9615  eluz2gt1  9930  1nuz2  9934  rpgt0  9994  ixxss1  10233  ixxss2  10234  ixxss12  10235  iccss2  10273  iccssico2  10276  elfzuz3  10352  uzdisj  10423  nn0disj  10468  zsupcllemstep  10585  zsupssdc  10594  addmodlteq  10756  expge0  10933  expge1  10934  expaddzaplem  10940  shftfn  11502  fsumf1o  12069  fsumge0  12138  fprodf1o  12267  bitsfzolem  12633  bezoutlemzz  12691  bezoutlemaz  12692  bezoutlembz  12693  bezoutlemsup  12698  1nprm  12804  nprm  12813  sqnprm  12826  dvdsprm  12827  coprm  12834  sqpweven  12865  2sqpwodd  12866  dfphi2  12910  phimullem  12915  eulerthlemrprm  12919  phisum  12931  expnprm  13044  1arith  13058  4sqlem18  13099  oddennn  13132  znnen  13138  ennnfonelemg  13143  ctinf  13170  mndid  13627  mhmf  13667  mhmlin  13669  mhm0  13670  grpinvex  13712  grplinv  13752  mulgz  13856  mulgdirlem  13859  mulgdir  13860  mulgass  13865  nsgbi  13910  nmzbi  13915  ghmf  13953  ghmlin  13954  conjnsg  13987  ablcmn  13997  cmncom  14008  crngmgp  14137  rhmmhm  14293  rhmghm  14296  rimf1o  14304  nzrnz  14316  subrgss  14356  subrg1cl  14363  rrgeq0i  14398  domneq0  14407  2idlelbas  14651  2idlcpblrng  14658  znidomb  14793  toponuni  14867  tpsuni  14886  neipsm  15006  cnf  15056  cnima  15072  txdis1cn  15130  hmeocnvcn  15158  psmetxrge0  15184  isxmet2d  15200  xmstopn  15307  mstopn  15308  bdxmet  15353  divcnap  15417  ivthinclemlr  15489  ivthinclemur  15491  dvlemap  15532  dvcnp2cntop  15551  dvaddxxbr  15553  dvmulxxbr  15554  dvcoapbr  15559  dvcjbr  15560  dvrecap  15565  dveflem  15578  plyf  15589  plyadd  15603  plymul  15604  plycn  15614  dvply2g  15618  dvdsppwf1o  15844  mpodvdsmulf1o  15845  lgsfle1  15869  lgsle1  15875  lgsdirprm  15894  lgsne0  15898  lgsquadlem1  15937  lgsquadlem2  15938  upgr1or2  16083  umgredg2en  16091  lfgredg2dom  16114  upgr2wlkdc  16359  trlres  16372  clwwlknon  16411  bj-indsuc  16685  nnsf  16770