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  589  pm5.62dc  951  3simpa  1018  xoror  1421  anxordi  1442  sbidm  1897  reurex  2750  eqimss  3278  eldifi  3326  elinel1  3390  inss1  3424  sopo  4405  wefr  4450  ordtr  4470  opelxp1  4754  relop  4875  ssrelrn  4917  funmo  5336  funrel  5338  funinsn  5373  fnfun  5421  ffn  5476  f1f  5536  f1of1  5576  f1ofo  5584  isof1o  5940  eqopi  6327  1st2nd2  6330  reldmtpos  6410  swoer  6721  ecopover  6793  ecopoverg  6796  fnfi  7119  casef  7271  nninff  7305  lpowlpo  7351  dfplpq2  7557  enq0ref  7636  cauappcvgprlemopl  7849  cauappcvgprlemdisj  7854  caucvgprlemopl  7872  caucvgprlemdisj  7877  caucvgprprlemopl  7900  caucvgprprlemopu  7902  caucvgprprlemdisj  7905  peano1nnnn  8055  axrnegex  8082  ltxrlt  8228  1nn  9137  zre  9466  nnssz  9479  ixxss1  10117  ixxss2  10118  ixxss12  10119  iccss2  10157  rge0ssre  10190  elfzuz  10234  uzdisj  10306  nn0disj  10351  frecuzrdgtcl  10651  frecuzrdgfunlem  10658  0wrd0  11115  modfsummodlemstep  11989  mertenslem2  12068  prmnn  12653  prmuz2  12674  oddpwdc  12717  sqpweven  12718  2sqpwodd  12719  phimullem  12768  hashgcdlem  12781  1arith  12911  ctinfom  13020  ctinf  13022  sgrpmgm  13461  mndsgrp  13475  grpmnd  13561  nsgsubg  13763  ghmgrp1  13803  ghmgrp2  13804  ablgrp  13847  cmnmnd  13859  crngring  13992  rimrhm  14156  subrgring  14209  subrgrcl  14211  rhmpropd  14239  domnnzr  14255  2idlelbas  14501  rng2idlsubgsubrng  14505  2idlcpblrng  14508  2idlcpbl  14509  qusrhm  14513  psr1clfi  14673  topontop  14709  tpstop  14730  cntop1  14896  cntop2  14897  hmeocn  15000  isxmet2d  15043  metxmet  15050  xmstps  15152  msxms  15153  xmsxmet  15155  msmet  15156  bdxmet  15196  ivthinclemlr  15332  ivthinclemur  15334  mpodvdsmulf1o  15685  uhgr0vb  15905  trliswlk  16156  bj-indint  16403  bj-inf2vnlem2  16443  peano4nninf  16486