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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used 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  4458  wefr  4503  ordtr  4523  opelxp1  4808  relop  4930  ssrelrn  4972  funmo  5392  funrel  5394  funinsn  5430  fnfun  5478  ffn  5533  f1f  5598  f1of1  5638  f1ofo  5646  isof1o  6013  eqopi  6406  1st2nd2  6409  reldmtpos  6524  swoer  6835  ecopover  6907  ecopoverg  6910  fnfi  7250  casef  7428  nninff  7462  lpowlpo  7508  papirr  7611  tapap  7616  dfplpq2  7721  enq0ref  7800  cauappcvgprlemopl  8013  cauappcvgprlemdisj  8018  caucvgprlemopl  8036  caucvgprlemdisj  8041  caucvgprprlemopl  8064  caucvgprprlemopu  8066  caucvgprprlemdisj  8069  peano1nnnn  8219  axrnegex  8246  ltxrlt  8391  1nn  9316  zre  9650  nnssz  9663  ixxss1  10308  ixxss2  10309  ixxss12  10310  iccss2  10348  rge0ssre  10381  elfzuz  10426  uzdisj  10502  nn0disj  10547  frecuzrdgtcl  10851  frecuzrdgfunlem  10858  0wrd0  11332  modfsummodlemstep  12226  mertenslem2  12305  prmnn  12890  prmuz2  12911  oddpwdc  12954  sqpweven  12955  2sqpwodd  12956  phimullem  13005  hashgcdlem  13018  1arith  13148  ballotfilem2  13230  ctinfom  13321  ctinf  13323  sgrpmgm  13724  mndsgrp  13736  grpmnd  13814  nsgsubg  14010  ghmgrp1  14050  ghmgrp2  14051  ablgrp  14094  cmnmnd  14106  crngring  14314  rimrhm  14480  subrgring  14534  subrgrcl  14536  rhmpropd  14564  domnnzr  14581  drnglring  14609  flddrngd  14617  2idlelbas  14855  rng2idlsubgsubrng  14859  2idlcpblrng  14862  2idlcpbl  14863  qusrhm  14867  assalmod  15008  assaring  15009  psr1clfi  15081  topontop  15117  tpstop  15138  cntop1  15304  cntop2  15305  hmeocn  15408  isxmet2d  15451  metxmet  15458  xmstps  15560  msxms  15561  xmsxmet  15563  msmet  15564  bdxmet  15604  ivthinclemlr  15740  ivthinclemur  15742  mpodvdsmulf1o  16110  uhgr0vb  16337  trliswlk  16639  eupthfi  16704  eupthistrl  16707  bj-indint  16969  bj-inf2vnlem2  17009  peano4nninf  17061  als-no-surprise  17159