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  954  sb1  1813  reurmo  2752  eldifn  3329  elinel2  3393  rabsnt  3747  eldifsni  3803  unimax  3928  ssintub  3947  exmidsssnc  4295  moop2  4346  wepo  4458  wetrep  4459  trssord  4479  ordelord  4480  ordsucim  4600  ordtri2or2exmidlem  4626  regexmidlem1  4633  reg2exmidlema  4634  tfis  4683  opelxp2  4762  funmo  5343  funopg  5362  funco  5368  funun  5373  fununi  5400  funimaexglem  5415  fndm  5431  frn  5493  f1ss  5551  f1ssr  5552  f1ssres  5554  forn  5565  f1f1orn  5597  f1orescnv  5602  f1imacnv  5603  funcocnv2  5611  funfveu  5655  nfvres  5678  isorel  5954  isoini2  5965  f1ofveu  6011  fovcld  6131  f1opw  6235  f1o2ndf1  6398  mpoxopn0yelv  6410  swoer  6735  mapsnconst  6868  en0  6974  en1  6978  phplem4  7046  phplem4dom  7053  phplem4on  7059  ssfilem  7067  ssfilemd  7069  diffitest  7081  inffiexmid  7103  supubti  7203  suplubti  7204  djuinr  7267  casefun  7289  casef1  7294  djufun  7308  nnnninfeq  7332  ctssexmid  7354  exmidonfinlem  7409  exmidfodomrlemim  7417  cc4f  7493  cc4n  7495  0npi  7538  mulclpi  7553  mulcanpig  7560  nlt1pig  7566  indpi  7567  nnppipi  7568  dfplpq2  7579  archnqq  7642  enq0tr  7659  nqnq0pi  7663  ltexprlemopl  7826  ltexprlemopu  7828  cauappcvgprlemopl  7871  cauappcvgprlemlol  7872  cauappcvgprlemopu  7873  cauappcvgprlemupu  7874  cauappcvgprlemdisj  7876  caucvgprlemopl  7894  caucvgprlemlol  7895  caucvgprlemopu  7896  caucvgprlemupu  7897  caucvgprlemdisj  7899  caucvgprprlemopl  7922  caucvgprprlemlol  7923  caucvgprprlemopu  7924  caucvgprprlemupu  7925  caucvgprprlemdisj  7927  suplocsrlempr  8032  ltresr2  8065  peano2nnnn  8078  axrnegex  8104  ltxrlt  8250  peano2nn  9160  elnn0z  9497  zaddcl  9524  ztri3or0  9526  eluz2gt1  9841  1nuz2  9845  rpgt0  9905  ixxss1  10144  ixxss2  10145  ixxss12  10146  iccss2  10184  iccssico2  10187  elfzuz3  10262  uzdisj  10333  nn0disj  10378  zsupcllemstep  10495  zsupssdc  10504  addmodlteq  10666  expge0  10843  expge1  10844  expaddzaplem  10850  shftfn  11407  fsumf1o  11974  fsumge0  12043  fprodf1o  12172  bitsfzolem  12538  bezoutlemzz  12596  bezoutlemaz  12597  bezoutlembz  12598  bezoutlemsup  12603  1nprm  12709  nprm  12718  sqnprm  12731  dvdsprm  12732  coprm  12739  sqpweven  12770  2sqpwodd  12771  dfphi2  12815  phimullem  12820  eulerthlemrprm  12824  phisum  12836  expnprm  12949  1arith  12963  4sqlem18  13004  oddennn  13036  znnen  13042  ennnfonelemg  13047  ctinf  13074  mndid  13531  mhmf  13571  mhmlin  13573  mhm0  13574  grpinvex  13616  grplinv  13656  mulgz  13760  mulgdirlem  13763  mulgdir  13764  mulgass  13769  nsgbi  13814  nmzbi  13819  ghmf  13857  ghmlin  13858  conjnsg  13891  ablcmn  13901  cmncom  13912  crngmgp  14041  rhmmhm  14197  rhmghm  14200  rimf1o  14208  nzrnz  14220  subrgss  14260  subrg1cl  14267  rrgeq0i  14302  domneq0  14310  2idlelbas  14554  2idlcpblrng  14561  znidomb  14696  toponuni  14768  tpsuni  14787  neipsm  14907  cnf  14957  cnima  14973  txdis1cn  15031  hmeocnvcn  15059  psmetxrge0  15085  isxmet2d  15101  xmstopn  15208  mstopn  15209  bdxmet  15254  divcnap  15318  ivthinclemlr  15390  ivthinclemur  15392  dvlemap  15433  dvcnp2cntop  15452  dvaddxxbr  15454  dvmulxxbr  15455  dvcoapbr  15460  dvcjbr  15461  dvrecap  15466  dveflem  15479  plyf  15490  plyadd  15504  plymul  15505  plycn  15515  dvply2g  15519  dvdsppwf1o  15742  mpodvdsmulf1o  15743  lgsfle1  15767  lgsle1  15773  lgsdirprm  15792  lgsne0  15796  lgsquadlem1  15835  lgsquadlem2  15836  upgr1or2  15981  umgredg2en  15989  lfgredg2dom  16012  upgr2wlkdc  16257  trlres  16270  clwwlknon  16309  bj-indsuc  16583  nnsf  16670