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  589  pm5.62dc  950  3simpa  999  xoror  1401  anxordi  1422  sbidm  1877  reurex  2730  eqimss  3258  eldifi  3306  elinel1  3370  inss1  3404  sopo  4381  wefr  4426  ordtr  4446  opelxp1  4730  relop  4849  ssrelrn  4891  funmo  5309  funrel  5311  funinsn  5346  fnfun  5394  ffn  5449  f1f  5507  f1of1  5547  f1ofo  5555  isof1o  5904  eqopi  6288  1st2nd2  6291  reldmtpos  6369  swoer  6678  ecopover  6750  ecopoverg  6753  fnfi  7071  casef  7223  nninff  7257  lpowlpo  7303  dfplpq2  7509  enq0ref  7588  cauappcvgprlemopl  7801  cauappcvgprlemdisj  7806  caucvgprlemopl  7824  caucvgprlemdisj  7829  caucvgprprlemopl  7852  caucvgprprlemopu  7854  caucvgprprlemdisj  7857  peano1nnnn  8007  axrnegex  8034  ltxrlt  8180  1nn  9089  zre  9418  nnssz  9431  ixxss1  10068  ixxss2  10069  ixxss12  10070  iccss2  10108  rge0ssre  10141  elfzuz  10185  uzdisj  10257  nn0disj  10302  frecuzrdgtcl  10601  frecuzrdgfunlem  10608  0wrd0  11064  modfsummodlemstep  11934  mertenslem2  12013  prmnn  12598  prmuz2  12619  oddpwdc  12662  sqpweven  12663  2sqpwodd  12664  phimullem  12713  hashgcdlem  12726  1arith  12856  ctinfom  12965  ctinf  12967  sgrpmgm  13406  mndsgrp  13420  grpmnd  13506  nsgsubg  13708  ghmgrp1  13748  ghmgrp2  13749  ablgrp  13792  cmnmnd  13804  crngring  13937  rimrhm  14100  subrgring  14153  subrgrcl  14155  rhmpropd  14183  domnnzr  14199  2idlelbas  14445  rng2idlsubgsubrng  14449  2idlcpblrng  14452  2idlcpbl  14453  qusrhm  14457  psr1clfi  14617  topontop  14653  tpstop  14674  cntop1  14840  cntop2  14841  hmeocn  14944  isxmet2d  14987  metxmet  14994  xmstps  15096  msxms  15097  xmsxmet  15099  msmet  15100  bdxmet  15140  ivthinclemlr  15276  ivthinclemur  15278  mpodvdsmulf1o  15629  uhgr0vb  15849  bj-indint  16204  bj-inf2vnlem2  16244  peano4nninf  16283