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  953  3simpa  1020  xoror  1423  anxordi  1444  sbidm  1899  reurex  2752  eqimss  3281  eldifi  3329  elinel1  3393  inss1  3427  sopo  4410  wefr  4455  ordtr  4475  opelxp1  4759  relop  4880  ssrelrn  4922  funmo  5341  funrel  5343  funinsn  5379  fnfun  5427  ffn  5482  f1f  5542  f1of1  5582  f1ofo  5590  isof1o  5948  eqopi  6335  1st2nd2  6338  reldmtpos  6419  swoer  6730  ecopover  6802  ecopoverg  6805  fnfi  7135  casef  7287  nninff  7321  lpowlpo  7367  dfplpq2  7574  enq0ref  7653  cauappcvgprlemopl  7866  cauappcvgprlemdisj  7871  caucvgprlemopl  7889  caucvgprlemdisj  7894  caucvgprprlemopl  7917  caucvgprprlemopu  7919  caucvgprprlemdisj  7922  peano1nnnn  8072  axrnegex  8099  ltxrlt  8245  1nn  9154  zre  9483  nnssz  9496  ixxss1  10139  ixxss2  10140  ixxss12  10141  iccss2  10179  rge0ssre  10212  elfzuz  10256  uzdisj  10328  nn0disj  10373  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  0wrd0  11140  modfsummodlemstep  12020  mertenslem2  12099  prmnn  12684  prmuz2  12705  oddpwdc  12748  sqpweven  12749  2sqpwodd  12750  phimullem  12799  hashgcdlem  12812  1arith  12942  ctinfom  13051  ctinf  13053  sgrpmgm  13492  mndsgrp  13506  grpmnd  13592  nsgsubg  13794  ghmgrp1  13834  ghmgrp2  13835  ablgrp  13878  cmnmnd  13890  crngring  14024  rimrhm  14188  subrgring  14241  subrgrcl  14243  rhmpropd  14271  domnnzr  14287  2idlelbas  14533  rng2idlsubgsubrng  14537  2idlcpblrng  14540  2idlcpbl  14541  qusrhm  14545  psr1clfi  14705  topontop  14741  tpstop  14762  cntop1  14928  cntop2  14929  hmeocn  15032  isxmet2d  15075  metxmet  15082  xmstps  15184  msxms  15185  xmsxmet  15187  msmet  15188  bdxmet  15228  ivthinclemlr  15364  ivthinclemur  15366  mpodvdsmulf1o  15717  uhgr0vb  15938  trliswlk  16240  eupthfi  16305  eupthistrl  16308  bj-indint  16547  bj-inf2vnlem2  16587  peano4nninf  16629