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  1898  reurex  2751  eqimss  3280  eldifi  3328  elinel1  3392  inss1  3426  sopo  4412  wefr  4457  ordtr  4477  opelxp1  4761  relop  4882  ssrelrn  4924  funmo  5343  funrel  5345  funinsn  5381  fnfun  5429  ffn  5484  f1f  5545  f1of1  5585  f1ofo  5593  isof1o  5953  eqopi  6340  1st2nd2  6343  reldmtpos  6424  swoer  6735  ecopover  6807  ecopoverg  6810  fnfi  7140  casef  7292  nninff  7326  lpowlpo  7372  dfplpq2  7579  enq0ref  7658  cauappcvgprlemopl  7871  cauappcvgprlemdisj  7876  caucvgprlemopl  7894  caucvgprlemdisj  7899  caucvgprprlemopl  7922  caucvgprprlemopu  7924  caucvgprprlemdisj  7927  peano1nnnn  8077  axrnegex  8104  ltxrlt  8250  1nn  9159  zre  9488  nnssz  9501  ixxss1  10144  ixxss2  10145  ixxss12  10146  iccss2  10184  rge0ssre  10217  elfzuz  10261  uzdisj  10333  nn0disj  10378  frecuzrdgtcl  10680  frecuzrdgfunlem  10687  0wrd0  11148  modfsummodlemstep  12041  mertenslem2  12120  prmnn  12705  prmuz2  12726  oddpwdc  12769  sqpweven  12770  2sqpwodd  12771  phimullem  12820  hashgcdlem  12833  1arith  12963  ctinfom  13072  ctinf  13074  sgrpmgm  13513  mndsgrp  13527  grpmnd  13613  nsgsubg  13815  ghmgrp1  13855  ghmgrp2  13856  ablgrp  13899  cmnmnd  13911  crngring  14045  rimrhm  14209  subrgring  14262  subrgrcl  14264  rhmpropd  14292  domnnzr  14308  2idlelbas  14554  rng2idlsubgsubrng  14558  2idlcpblrng  14561  2idlcpbl  14562  qusrhm  14566  psr1clfi  14731  topontop  14767  tpstop  14788  cntop1  14954  cntop2  14955  hmeocn  15058  isxmet2d  15101  metxmet  15108  xmstps  15210  msxms  15211  xmsxmet  15213  msmet  15214  bdxmet  15254  ivthinclemlr  15390  ivthinclemur  15392  mpodvdsmulf1o  15743  uhgr0vb  15964  trliswlk  16266  eupthfi  16331  eupthistrl  16334  bj-indint  16586  bj-inf2vnlem2  16626  peano4nninf  16671