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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.63dc  959  sb1  1819  reurmo  2772  eldifn  3352  elinel2  3416  rabsnt  3786  eldifsni  3843  unimax  3969  ssintub  3988  exmidsssnc  4340  moop2  4392  wepo  4504  wetrep  4505  trssord  4525  ordelord  4526  ordsucim  4647  ordtri2or2exmidlem  4673  regexmidlem1  4680  reg2exmidlema  4681  tfis  4730  opelxp2  4809  funmo  5392  funopg  5411  funco  5417  funun  5422  fununi  5449  funimaexglem  5464  fndm  5480  frn  5542  f1ss  5604  f1ssr  5605  f1ssres  5607  forn  5618  f1f1orn  5650  f1orescnv  5655  f1imacnv  5656  funcocnv2  5664  funfveu  5708  nfvres  5732  isorel  6014  isoini2  6025  f1ofveu  6073  fovcld  6193  f1opw  6297  f1o2ndf1  6464  mpoxopn0yelv  6510  swoer  6835  mapsnconst  6976  en0  7082  en1  7086  phplem4  7156  phplem4dom  7163  phplem4on  7169  ssfilem  7177  ssfilemd  7179  diffitest  7191  inffiexmid  7213  fsuppcorn  7301  supubti  7340  suplubti  7341  djuinr  7404  casefun  7426  casef1  7431  djufun  7445  nnnninfeq  7469  ctssexmid  7491  exmidonfinlem  7546  exmidfodomrlemim  7554  cc4f  7636  cc4n  7638  0npi  7681  mulclpi  7696  mulcanpig  7703  nlt1pig  7709  indpi  7710  nnppipi  7711  dfplpq2  7722  archnqq  7785  enq0tr  7802  nqnq0pi  7806  ltexprlemopl  7969  ltexprlemopu  7971  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemupu  8017  cauappcvgprlemdisj  8019  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemupu  8040  caucvgprlemdisj  8042  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemupu  8068  caucvgprprlemdisj  8070  suplocsrlempr  8175  ltresr2  8208  peano2nnnn  8221  axrnegex  8247  ltxrlt  8392  peano2nn  9319  elnn0z  9662  zaddcl  9689  ztri3or0  9691  eluz2gt1  10012  1nuz2  10016  rpgt0  10077  ixxss1  10317  ixxss2  10318  ixxss12  10319  iccss2  10357  iccssico2  10360  elfzuz3  10436  uzdisj  10511  nn0disj  10556  zsupcllemstep  10673  zsupssdc  10684  addmodlteq  10849  expge0  11026  expge1  11027  expaddzaplem  11033  shftfn  11604  fsumf1o  12175  fsumge0  12244  fprodf1o  12373  bitsfzolem  12739  bezoutlemzz  12797  bezoutlemaz  12798  bezoutlembz  12799  bezoutlemsup  12804  1nprm  12910  nprm  12919  sqnprm  12933  dvdsprm  12934  coprm  12941  sqpweven  12973  2sqpwodd  12974  dfphi2  13020  phimullem  13025  eulerthlemrprm  13029  phisum  13041  expnprm  13154  1arith  13168  4sqlem18  13209  ballotfilem4  13292  ballotfilem5  13293  ballotfilemfrc  13321  ballotfilemirc  13326  ballotfilemth  13332  oddennn  13334  znnen  13340  ennnfonelemg  13345  ctinf  13372  mndid  13789  mhmf  13823  mhmlin  13825  mhm0  13826  grpinvex  13866  grplinv  13906  mulgz  14004  mulgdirlem  14007  mulgdir  14008  mulgass  14013  nsgbi  14058  nmzbi  14063  ghmf  14101  ghmlin  14102  conjnsg  14135  ablcmn  14145  cmncom  14156  crngmgp  14359  rhmmhm  14517  rhmghm  14520  rimf1o  14528  nzrnz  14540  subrgss  14581  subrg1cl  14588  rrgeq0i  14623  domneq0  14632  fldcrngd  14667  2idlelbas  14904  2idlcpblrng  14911  znidomb  15044  assalem  15054  toponuni  15168  tpsuni  15187  neipsm  15307  cnf  15357  cnima  15373  txdis1cn  15431  hmeocnvcn  15459  psmetxrge0  15485  isxmet2d  15501  xmstopn  15608  mstopn  15609  bdxmet  15654  divcnap  15718  ivthinclemlr  15790  ivthinclemur  15792  dvlemap  15833  dvcnp2cntop  15852  dvaddxxbr  15854  dvmulxxbr  15855  dvcoapbr  15860  dvcjbr  15861  dvrecap  15866  dveflem  15879  plyf  15890  plyadd  15904  plymul  15905  plycn  15915  dvply2g  15919  efnnfsumcl  16161  efchtqdvds  16187  dvdsppwf1o  16205  mpodvdsmulf1o  16206  lgsfle1  16250  lgsle1  16256  lgsdirprm  16275  lgsne0  16279  lgsquadlem1  16318  lgsquadlem2  16319  upgr1or2  16464  umgredg2en  16472  lfgredg2dom  16495  upgr2wlkdc  16740  trlres  16753  clwwlknon  16792  bj-indsuc  17076  nnsf  17170  als-no-surprise  17269  alseueu  17300