Theorem simplbi 274

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simplbi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simplbi	⊢ (𝜑 → 𝜓)

Proof of Theorem simplbi

Step	Hyp	Ref	Expression
1		simplbi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	biimpi 120	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 112	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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an3  591  pm5.62dc  954  3simpa  1021  xoror  1424  anxordi  1445  sbidm  1900  reurex  2762  eqimss  3291  eldifi  3340  elinel1  3404  inss1  3440  sopo  4433  wefr  4478  ordtr  4498  opelxp1  4782  relop  4904  ssrelrn  4946  funmo  5366  funrel  5368  funinsn  5404  fnfun  5452  ffn  5507  f1f  5572  f1of1  5612  f1ofo  5620  isof1o  5979  eqopi  6365  1st2nd2  6368  reldmtpos  6483  swoer  6794  ecopover  6866  ecopoverg  6869  fnfi  7202  casef  7378  nninff  7412  lpowlpo  7458  dfplpq2  7665  enq0ref  7744  cauappcvgprlemopl  7957  cauappcvgprlemdisj  7962  caucvgprlemopl  7980  caucvgprlemdisj  7985  caucvgprprlemopl  8008  caucvgprprlemopu  8010  caucvgprprlemdisj  8013  peano1nnnn  8163  axrnegex  8190  ltxrlt  8335  1nn  9244  zre  9577  nnssz  9590  ixxss1  10233  ixxss2  10234  ixxss12  10235  iccss2  10273  rge0ssre  10306  elfzuz  10351  uzdisj  10423  nn0disj  10468  frecuzrdgtcl  10770  frecuzrdgfunlem  10777  0wrd0  11243  modfsummodlemstep  12136  mertenslem2  12215  prmnn  12800  prmuz2  12821  oddpwdc  12864  sqpweven  12865  2sqpwodd  12866  phimullem  12915  hashgcdlem  12928  1arith  13058  ctinfom  13168  ctinf  13170  sgrpmgm  13609  mndsgrp  13623  grpmnd  13709  nsgsubg  13911  ghmgrp1  13951  ghmgrp2  13952  ablgrp  13995  cmnmnd  14007  crngring  14141  rimrhm  14305  subrgring  14358  subrgrcl  14360  rhmpropd  14388  domnnzr  14405  2idlelbas  14651  rng2idlsubgsubrng  14655  2idlcpblrng  14658  2idlcpbl  14659  qusrhm  14663  psr1clfi  14830  topontop  14866  tpstop  14887  cntop1  15053  cntop2  15054  hmeocn  15157  isxmet2d  15200  metxmet  15207  xmstps  15309  msxms  15310  xmsxmet  15312  msmet  15313  bdxmet  15353  ivthinclemlr  15489  ivthinclemur  15491  mpodvdsmulf1o  15845  uhgr0vb  16066  trliswlk  16368  eupthfi  16433  eupthistrl  16436  bj-indint  16688  bj-inf2vnlem2  16728  peano4nninf  16771