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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  an3  595  pm5.62dc  958  3simpa  1025  xoror  1428  anxordi  1449  sbidm  1904  reurex  2771  eqimss  3302  eldifi  3351  elinel1  3415  inss1  3451  sopo  4460  wefr  4505  ordtr  4525  opelxp1  4810  relop  4932  ssrelrn  4974  funmo  5395  funrel  5397  funinsn  5433  fnfun  5481  ffn  5536  f1f  5601  f1of1  5641  f1ofo  5649  isof1o  6016  eqopi  6410  1st2nd2  6413  reldmtpos  6529  swoer  6840  ecopover  6912  ecopoverg  6915  fnfi  7256  casef  7434  nninff  7468  lpowlpo  7514  papirr  7617  tapap  7622  dfplpq2  7727  enq0ref  7806  cauappcvgprlemopl  8019  cauappcvgprlemdisj  8024  caucvgprlemopl  8042  caucvgprlemdisj  8047  caucvgprprlemopl  8070  caucvgprprlemopu  8072  caucvgprprlemdisj  8075  peano1nnnn  8225  axrnegex  8252  ltxrlt  8397  1nn  9324  zre  9657  nnssz  9670  ixxss1  10322  ixxss2  10323  ixxss12  10324  iccss2  10362  rge0ssre  10395  elfzuz  10440  uzdisj  10516  nn0disj  10561  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  0wrd0  11351  modfsummodlemstep  12248  mertenslem2  12327  prmnn  12912  prmuz2  12934  nnmaxpw  12977  sqpweven  12979  2sqpwodd  12980  phimullem  13031  hashgcdlem  13044  1arith  13174  ballotfilem2  13285  ctinfom  13376  ctinf  13378  sgrpmgm  13780  mndsgrp  13792  grpmnd  13870  nsgsubg  14066  ghmgrp1  14106  ghmgrp2  14107  ablgrp  14181  cmnmnd  14193  crngring  14418  rimrhm  14586  subrgring  14640  subrgrcl  14642  rhmpropd  14670  domnnzr  14687  drnglring  14715  flddrngd  14723  2idlelbas  14961  rng2idlsubgsubrng  14965  2idlcpblrng  14968  2idlcpbl  14969  qusrhm  14973  assalmod  15114  assaring  15115  psr1clfi  15207  topontop  15257  tpstop  15278  cntop1  15444  cntop2  15445  hmeocn  15548  isxmet2d  15591  metxmet  15598  xmstps  15700  msxms  15701  xmsxmet  15703  msmet  15704  bdxmet  15744  ivthinclemlr  15880  ivthinclemur  15882  mpodvdsmulf1o  16301  uhgr0vb  16547  trliswlk  16849  eupthfi  16914  eupthistrl  16917  bj-indint  17179  bj-inf2vnlem2  17219  peano4nninf  17272  als-no-surprise  17371