Theorem simplbi 274

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simplbi.1	|- ( ph <-> ( ps /\ ch ) )

Assertion

Ref	Expression
simplbi	|- ( ph -> ps )

Proof of Theorem simplbi

Step	Hyp	Ref	Expression
1		simplbi.1	. . 3 |- ( ph <-> ( ps /\ ch ) )
2	1	biimpi 120	. 2 |- ( ph -> ( ps /\ ch ) )
3	2	simpld 112	1 |- ( ph -> ps )

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  1899  reurex  2753  eqimss  3282  eldifi  3331  elinel1  3395  inss1  3429  sopo  4416  wefr  4461  ordtr  4481  opelxp1  4765  relop  4886  ssrelrn  4928  funmo  5348  funrel  5350  funinsn  5386  fnfun  5434  ffn  5489  f1f  5551  f1of1  5591  f1ofo  5599  isof1o  5958  eqopi  6344  1st2nd2  6347  reldmtpos  6462  swoer  6773  ecopover  6845  ecopoverg  6848  fnfi  7178  casef  7330  nninff  7364  lpowlpo  7410  dfplpq2  7617  enq0ref  7696  cauappcvgprlemopl  7909  cauappcvgprlemdisj  7914  caucvgprlemopl  7932  caucvgprlemdisj  7937  caucvgprprlemopl  7960  caucvgprprlemopu  7962  caucvgprprlemdisj  7965  peano1nnnn  8115  axrnegex  8142  ltxrlt  8287  1nn  9196  zre  9527  nnssz  9540  ixxss1  10183  ixxss2  10184  ixxss12  10185  iccss2  10223  rge0ssre  10256  elfzuz  10301  uzdisj  10373  nn0disj  10418  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  0wrd0  11188  modfsummodlemstep  12081  mertenslem2  12160  prmnn  12745  prmuz2  12766  oddpwdc  12809  sqpweven  12810  2sqpwodd  12811  phimullem  12860  hashgcdlem  12873  1arith  13003  ctinfom  13112  ctinf  13114  sgrpmgm  13553  mndsgrp  13567  grpmnd  13653  nsgsubg  13855  ghmgrp1  13895  ghmgrp2  13896  ablgrp  13939  cmnmnd  13951  crngring  14085  rimrhm  14249  subrgring  14302  subrgrcl  14304  rhmpropd  14332  domnnzr  14349  2idlelbas  14595  rng2idlsubgsubrng  14599  2idlcpblrng  14602  2idlcpbl  14603  qusrhm  14607  psr1clfi  14772  topontop  14808  tpstop  14829  cntop1  14995  cntop2  14996  hmeocn  15099  isxmet2d  15142  metxmet  15149  xmstps  15251  msxms  15252  xmsxmet  15254  msmet  15255  bdxmet  15295  ivthinclemlr  15431  ivthinclemur  15433  mpodvdsmulf1o  15787  uhgr0vb  16008  trliswlk  16310  eupthfi  16375  eupthistrl  16378  bj-indint  16630  bj-inf2vnlem2  16670  peano4nninf  16715