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  952  sb1  1812  reurmo  2751  eldifn  3327  elinel2  3391  rabsnt  3741  eldifsni  3797  unimax  3922  ssintub  3941  exmidsssnc  4288  moop2  4339  wepo  4451  wetrep  4452  trssord  4472  ordelord  4473  ordsucim  4593  ordtri2or2exmidlem  4619  regexmidlem1  4626  reg2exmidlema  4627  tfis  4676  opelxp2  4755  funmo  5336  funopg  5355  funco  5361  funun  5365  fununi  5392  funimaexglem  5407  fndm  5423  frn  5485  f1ss  5542  f1ssr  5543  f1ssres  5545  forn  5556  f1f1orn  5588  f1orescnv  5593  f1imacnv  5594  funcocnv2  5602  funfveu  5645  nfvres  5668  isorel  5941  isoini2  5952  f1ofveu  5998  fovcld  6118  f1opw  6222  f1o2ndf1  6385  mpoxopn0yelv  6396  swoer  6721  mapsnconst  6854  en0  6960  en1  6964  phplem4  7029  phplem4dom  7036  phplem4on  7042  ssfilem  7050  diffitest  7062  inffiexmid  7084  supubti  7182  suplubti  7183  djuinr  7246  casefun  7268  casef1  7273  djufun  7287  nnnninfeq  7311  ctssexmid  7333  exmidonfinlem  7387  exmidfodomrlemim  7395  cc4f  7471  cc4n  7473  0npi  7516  mulclpi  7531  mulcanpig  7538  nlt1pig  7544  indpi  7545  nnppipi  7546  dfplpq2  7557  archnqq  7620  enq0tr  7637  nqnq0pi  7641  ltexprlemopl  7804  ltexprlemopu  7806  cauappcvgprlemopl  7849  cauappcvgprlemlol  7850  cauappcvgprlemopu  7851  cauappcvgprlemupu  7852  cauappcvgprlemdisj  7854  caucvgprlemopl  7872  caucvgprlemlol  7873  caucvgprlemopu  7874  caucvgprlemupu  7875  caucvgprlemdisj  7877  caucvgprprlemopl  7900  caucvgprprlemlol  7901  caucvgprprlemopu  7902  caucvgprprlemupu  7903  caucvgprprlemdisj  7905  suplocsrlempr  8010  ltresr2  8043  peano2nnnn  8056  axrnegex  8082  ltxrlt  8228  peano2nn  9138  elnn0z  9475  zaddcl  9502  ztri3or0  9504  eluz2gt1  9814  1nuz2  9818  rpgt0  9878  ixxss1  10117  ixxss2  10118  ixxss12  10119  iccss2  10157  iccssico2  10160  elfzuz3  10235  uzdisj  10306  nn0disj  10351  zsupcllemstep  10466  zsupssdc  10475  addmodlteq  10637  expge0  10814  expge1  10815  expaddzaplem  10821  shftfn  11356  fsumf1o  11922  fsumge0  11991  fprodf1o  12120  bitsfzolem  12486  bezoutlemzz  12544  bezoutlemaz  12545  bezoutlembz  12546  bezoutlemsup  12551  1nprm  12657  nprm  12666  sqnprm  12679  dvdsprm  12680  coprm  12687  sqpweven  12718  2sqpwodd  12719  dfphi2  12763  phimullem  12768  eulerthlemrprm  12772  phisum  12784  expnprm  12897  1arith  12911  4sqlem18  12952  oddennn  12984  znnen  12990  ennnfonelemg  12995  ctinf  13022  mndid  13479  mhmf  13519  mhmlin  13521  mhm0  13522  grpinvex  13564  grplinv  13604  mulgz  13708  mulgdirlem  13711  mulgdir  13712  mulgass  13717  nsgbi  13762  nmzbi  13767  ghmf  13805  ghmlin  13806  conjnsg  13839  ablcmn  13849  cmncom  13860  crngmgp  13988  rhmmhm  14144  rhmghm  14147  rimf1o  14155  nzrnz  14167  subrgss  14207  subrg1cl  14214  rrgeq0i  14249  domneq0  14257  2idlelbas  14501  2idlcpblrng  14508  znidomb  14643  toponuni  14710  tpsuni  14729  neipsm  14849  cnf  14899  cnima  14915  txdis1cn  14973  hmeocnvcn  15001  psmetxrge0  15027  isxmet2d  15043  xmstopn  15150  mstopn  15151  bdxmet  15196  divcnap  15260  ivthinclemlr  15332  ivthinclemur  15334  dvlemap  15375  dvcnp2cntop  15394  dvaddxxbr  15396  dvmulxxbr  15397  dvcoapbr  15402  dvcjbr  15403  dvrecap  15408  dveflem  15421  plyf  15432  plyadd  15446  plymul  15447  plycn  15457  dvply2g  15461  dvdsppwf1o  15684  mpodvdsmulf1o  15685  lgsfle1  15709  lgsle1  15715  lgsdirprm  15734  lgsne0  15738  lgsquadlem1  15777  lgsquadlem2  15778  upgr1or2  15922  umgredg2en  15930  lfgredg2dom  15951  upgr2wlkdc  16147  trlres  16159  bj-indsuc  16400  nnsf  16485