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  1900  reurex  2763  eqimss  3292  eldifi  3341  elinel1  3405  inss1  3441  sopo  4434  wefr  4479  ordtr  4499  opelxp1  4783  relop  4905  ssrelrn  4947  funmo  5367  funrel  5369  funinsn  5405  fnfun  5453  ffn  5508  f1f  5573  f1of1  5613  f1ofo  5621  isof1o  5980  eqopi  6366  1st2nd2  6369  reldmtpos  6484  swoer  6795  ecopover  6867  ecopoverg  6870  fnfi  7203  casef  7379  nninff  7413  lpowlpo  7459  papirr  7560  dfplpq2  7669  enq0ref  7748  cauappcvgprlemopl  7961  cauappcvgprlemdisj  7966  caucvgprlemopl  7984  caucvgprlemdisj  7989  caucvgprprlemopl  8012  caucvgprprlemopu  8014  caucvgprprlemdisj  8017  peano1nnnn  8167  axrnegex  8194  ltxrlt  8339  1nn  9248  zre  9581  nnssz  9594  ixxss1  10237  ixxss2  10238  ixxss12  10239  iccss2  10277  rge0ssre  10310  elfzuz  10355  uzdisj  10427  nn0disj  10472  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  0wrd0  11250  modfsummodlemstep  12143  mertenslem2  12222  prmnn  12807  prmuz2  12828  oddpwdc  12871  sqpweven  12872  2sqpwodd  12873  phimullem  12922  hashgcdlem  12935  1arith  13065  ballotfilem2  13142  ctinfom  13179  ctinf  13181  sgrpmgm  13620  mndsgrp  13634  grpmnd  13720  nsgsubg  13922  ghmgrp1  13962  ghmgrp2  13963  ablgrp  14006  cmnmnd  14018  crngring  14152  rimrhm  14316  subrgring  14369  subrgrcl  14371  rhmpropd  14399  domnnzr  14416  2idlelbas  14664  rng2idlsubgsubrng  14668  2idlcpblrng  14671  2idlcpbl  14672  qusrhm  14676  psr1clfi  14843  topontop  14879  tpstop  14900  cntop1  15066  cntop2  15067  hmeocn  15170  isxmet2d  15213  metxmet  15220  xmstps  15322  msxms  15323  xmsxmet  15325  msmet  15326  bdxmet  15366  ivthinclemlr  15502  ivthinclemur  15504  mpodvdsmulf1o  15858  uhgr0vb  16079  trliswlk  16381  eupthfi  16446  eupthistrl  16449  bj-indint  16701  bj-inf2vnlem2  16741  peano4nninf  16784