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:  pm5.62dc  947  3simpa  996  xoror  1390  anxordi  1411  sbidm  1862  reurex  2712  eqimss  3233  eldifi  3281  elinel1  3345  inss1  3379  sopo  4344  wefr  4389  ordtr  4409  opelxp1  4693  relop  4812  funmo  5269  funrel  5271  funinsn  5303  fnfun  5351  ffn  5403  f1f  5459  f1of1  5499  f1ofo  5507  isof1o  5850  eqopi  6225  1st2nd2  6228  reldmtpos  6306  swoer  6615  ecopover  6687  ecopoverg  6690  fnfi  6995  casef  7147  nninff  7181  lpowlpo  7227  dfplpq2  7414  enq0ref  7493  cauappcvgprlemopl  7706  cauappcvgprlemdisj  7711  caucvgprlemopl  7729  caucvgprlemdisj  7734  caucvgprprlemopl  7757  caucvgprprlemopu  7759  caucvgprprlemdisj  7762  peano1nnnn  7912  axrnegex  7939  ltxrlt  8085  1nn  8993  zre  9321  nnssz  9334  ixxss1  9970  ixxss2  9971  ixxss12  9972  iccss2  10010  rge0ssre  10043  elfzuz  10087  uzdisj  10159  nn0disj  10204  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  0wrd0  10940  modfsummodlemstep  11600  mertenslem2  11679  prmnn  12248  prmuz2  12269  oddpwdc  12312  sqpweven  12313  2sqpwodd  12314  phimullem  12363  hashgcdlem  12376  1arith  12505  ctinfom  12585  ctinf  12587  sgrpmgm  12990  mndsgrp  13002  grpmnd  13079  nsgsubg  13275  ghmgrp1  13315  ghmgrp2  13316  ablgrp  13359  cmnmnd  13371  crngring  13504  rimrhm  13667  subrgring  13720  subrgrcl  13722  rhmpropd  13750  domnnzr  13766  2idlelbas  14012  rng2idlsubgsubrng  14016  2idlcpblrng  14019  2idlcpbl  14020  qusrhm  14024  topontop  14182  tpstop  14203  cntop1  14369  cntop2  14370  hmeocn  14473  isxmet2d  14516  metxmet  14523  xmstps  14625  msxms  14626  xmsxmet  14628  msmet  14629  bdxmet  14669  ivthinclemlr  14791  ivthinclemur  14793  bj-indint  15423  bj-inf2vnlem2  15463  peano4nninf  15496