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  2765  eqimss  3294  eldifi  3343  elinel1  3407  inss1  3443  sopo  4436  wefr  4481  ordtr  4501  opelxp1  4785  relop  4907  ssrelrn  4949  funmo  5369  funrel  5371  funinsn  5407  fnfun  5455  ffn  5510  f1f  5575  f1of1  5615  f1ofo  5623  isof1o  5982  eqopi  6368  1st2nd2  6371  reldmtpos  6486  swoer  6797  ecopover  6869  ecopoverg  6872  fnfi  7205  casef  7381  nninff  7415  lpowlpo  7461  papirr  7564  tapap  7569  dfplpq2  7674  enq0ref  7753  cauappcvgprlemopl  7966  cauappcvgprlemdisj  7971  caucvgprlemopl  7989  caucvgprlemdisj  7994  caucvgprprlemopl  8017  caucvgprprlemopu  8019  caucvgprprlemdisj  8022  peano1nnnn  8172  axrnegex  8199  ltxrlt  8344  1nn  9253  zre  9586  nnssz  9599  ixxss1  10243  ixxss2  10244  ixxss12  10245  iccss2  10283  rge0ssre  10316  elfzuz  10361  uzdisj  10434  nn0disj  10479  frecuzrdgtcl  10781  frecuzrdgfunlem  10788  0wrd0  11258  modfsummodlemstep  12151  mertenslem2  12230  prmnn  12815  prmuz2  12836  oddpwdc  12879  sqpweven  12880  2sqpwodd  12881  phimullem  12930  hashgcdlem  12943  1arith  13073  ballotfilem2  13153  ctinfom  13200  ctinf  13202  sgrpmgm  13641  mndsgrp  13655  grpmnd  13741  nsgsubg  13943  ghmgrp1  13983  ghmgrp2  13984  ablgrp  14027  cmnmnd  14039  crngring  14173  rimrhm  14338  subrgring  14392  subrgrcl  14394  rhmpropd  14422  domnnzr  14439  drnglring  14467  flddrngd  14475  2idlelbas  14713  rng2idlsubgsubrng  14717  2idlcpblrng  14720  2idlcpbl  14721  qusrhm  14725  psr1clfi  14892  topontop  14928  tpstop  14949  cntop1  15115  cntop2  15116  hmeocn  15219  isxmet2d  15262  metxmet  15269  xmstps  15371  msxms  15372  xmsxmet  15374  msmet  15375  bdxmet  15415  ivthinclemlr  15551  ivthinclemur  15553  mpodvdsmulf1o  15907  uhgr0vb  16128  trliswlk  16430  eupthfi  16495  eupthistrl  16498  bj-indint  16750  bj-inf2vnlem2  16790  peano4nninf  16833