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  595  pm5.62dc  958  3simpa  1025  xoror  1428  anxordi  1449  sbidm  1904  reurex  2771  eqimss  3302  eldifi  3351  elinel1  3415  inss1  3451  sopo  4456  wefr  4501  ordtr  4521  opelxp1  4806  relop  4928  ssrelrn  4970  funmo  5390  funrel  5392  funinsn  5428  fnfun  5476  ffn  5531  f1f  5596  f1of1  5636  f1ofo  5644  isof1o  6007  eqopi  6400  1st2nd2  6403  reldmtpos  6518  swoer  6829  ecopover  6901  ecopoverg  6904  fnfi  7244  casef  7422  nninff  7456  lpowlpo  7502  papirr  7605  tapap  7610  dfplpq2  7715  enq0ref  7794  cauappcvgprlemopl  8007  cauappcvgprlemdisj  8012  caucvgprlemopl  8030  caucvgprlemdisj  8035  caucvgprprlemopl  8058  caucvgprprlemopu  8060  caucvgprprlemdisj  8063  peano1nnnn  8213  axrnegex  8240  ltxrlt  8385  1nn  9298  zre  9631  nnssz  9644  ixxss1  10289  ixxss2  10290  ixxss12  10291  iccss2  10329  rge0ssre  10362  elfzuz  10407  uzdisj  10483  nn0disj  10528  frecuzrdgtcl  10832  frecuzrdgfunlem  10839  0wrd0  11313  modfsummodlemstep  12207  mertenslem2  12286  prmnn  12871  prmuz2  12892  oddpwdc  12935  sqpweven  12936  2sqpwodd  12937  phimullem  12986  hashgcdlem  12999  1arith  13129  ballotfilem2  13211  ctinfom  13302  ctinf  13304  sgrpmgm  13705  mndsgrp  13717  grpmnd  13795  nsgsubg  13991  ghmgrp1  14031  ghmgrp2  14032  ablgrp  14075  cmnmnd  14087  crngring  14295  rimrhm  14461  subrgring  14515  subrgrcl  14517  rhmpropd  14545  domnnzr  14562  drnglring  14590  flddrngd  14598  2idlelbas  14836  rng2idlsubgsubrng  14840  2idlcpblrng  14843  2idlcpbl  14844  qusrhm  14848  assalmod  14989  assaring  14990  psr1clfi  15062  topontop  15098  tpstop  15119  cntop1  15285  cntop2  15286  hmeocn  15389  isxmet2d  15432  metxmet  15439  xmstps  15541  msxms  15542  xmsxmet  15544  msmet  15545  bdxmet  15585  ivthinclemlr  15721  ivthinclemur  15723  mpodvdsmulf1o  16087  uhgr0vb  16308  trliswlk  16610  eupthfi  16675  eupthistrl  16678  bj-indint  16940  bj-inf2vnlem2  16980  peano4nninf  17023  als-no-surprise  17121