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:  pm5.62dc  948  3simpa  997  xoror  1399  anxordi  1420  sbidm  1875  reurex  2725  eqimss  3248  eldifi  3296  elinel1  3360  inss1  3394  sopo  4364  wefr  4409  ordtr  4429  opelxp1  4713  relop  4832  ssrelrn  4874  funmo  5291  funrel  5293  funinsn  5328  fnfun  5376  ffn  5431  f1f  5488  f1of1  5528  f1ofo  5536  isof1o  5883  eqopi  6265  1st2nd2  6268  reldmtpos  6346  swoer  6655  ecopover  6727  ecopoverg  6730  fnfi  7045  casef  7197  nninff  7231  lpowlpo  7277  dfplpq2  7474  enq0ref  7553  cauappcvgprlemopl  7766  cauappcvgprlemdisj  7771  caucvgprlemopl  7789  caucvgprlemdisj  7794  caucvgprprlemopl  7817  caucvgprprlemopu  7819  caucvgprprlemdisj  7822  peano1nnnn  7972  axrnegex  7999  ltxrlt  8145  1nn  9054  zre  9383  nnssz  9396  ixxss1  10033  ixxss2  10034  ixxss12  10035  iccss2  10073  rge0ssre  10106  elfzuz  10150  uzdisj  10222  nn0disj  10267  frecuzrdgtcl  10564  frecuzrdgfunlem  10571  0wrd0  11027  modfsummodlemstep  11812  mertenslem2  11891  prmnn  12476  prmuz2  12497  oddpwdc  12540  sqpweven  12541  2sqpwodd  12542  phimullem  12591  hashgcdlem  12604  1arith  12734  ctinfom  12843  ctinf  12845  sgrpmgm  13283  mndsgrp  13297  grpmnd  13383  nsgsubg  13585  ghmgrp1  13625  ghmgrp2  13626  ablgrp  13669  cmnmnd  13681  crngring  13814  rimrhm  13977  subrgring  14030  subrgrcl  14032  rhmpropd  14060  domnnzr  14076  2idlelbas  14322  rng2idlsubgsubrng  14326  2idlcpblrng  14329  2idlcpbl  14330  qusrhm  14334  psr1clfi  14494  topontop  14530  tpstop  14551  cntop1  14717  cntop2  14718  hmeocn  14821  isxmet2d  14864  metxmet  14871  xmstps  14973  msxms  14974  xmsxmet  14976  msmet  14977  bdxmet  15017  ivthinclemlr  15153  ivthinclemur  15155  mpodvdsmulf1o  15506  uhgr0vb  15724  bj-indint  15941  bj-inf2vnlem2  15981  peano4nninf  16017