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:  pm5.62dc  947  3simpa  996  xoror  1390  anxordi  1411  sbidm  1862  reurex  2704  eqimss  3224  eldifi  3272  elinel1  3336  inss1  3370  sopo  4328  wefr  4373  ordtr  4393  opelxp1  4675  relop  4792  funmo  5246  funrel  5248  funinsn  5280  fnfun  5328  ffn  5380  f1f  5436  f1of1  5475  f1ofo  5483  isof1o  5824  eqopi  6191  1st2nd2  6194  reldmtpos  6272  swoer  6581  ecopover  6651  ecopoverg  6654  fnfi  6954  casef  7105  nninff  7139  lpowlpo  7184  dfplpq2  7371  enq0ref  7450  cauappcvgprlemopl  7663  cauappcvgprlemdisj  7668  caucvgprlemopl  7686  caucvgprlemdisj  7691  caucvgprprlemopl  7714  caucvgprprlemopu  7716  caucvgprprlemdisj  7719  peano1nnnn  7869  axrnegex  7896  ltxrlt  8041  1nn  8948  zre  9275  nnssz  9288  ixxss1  9922  ixxss2  9923  ixxss12  9924  iccss2  9962  rge0ssre  9995  elfzuz  10039  uzdisj  10111  nn0disj  10156  frecuzrdgtcl  10430  frecuzrdgfunlem  10437  modfsummodlemstep  11483  mertenslem2  11562  prmnn  12128  prmuz2  12149  oddpwdc  12192  sqpweven  12193  2sqpwodd  12194  phimullem  12243  hashgcdlem  12256  1arith  12383  ctinfom  12447  ctinf  12449  sgrpmgm  12836  mndsgrp  12848  grpmnd  12918  nsgsubg  13110  ghmgrp1  13145  ghmgrp2  13146  ablgrp  13189  cmnmnd  13201  crngring  13323  rimrhm  13482  subrgring  13532  subrgrcl  13534  2idlelbas  13792  rng2idlsubgsubrng  13796  2idlcpblrng  13799  2idlcpbl  13800  topontop  13911  tpstop  13932  cntop1  14098  cntop2  14099  hmeocn  14202  isxmet2d  14245  metxmet  14252  xmstps  14354  msxms  14355  xmsxmet  14357  msmet  14358  bdxmet  14398  ivthinclemlr  14512  ivthinclemur  14514  bj-indint  15080  bj-inf2vnlem2  15120  peano4nninf  15153