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  6528  swoer  6839  ecopover  6911  ecopoverg  6914  fnfi  7254  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  9659  nnssz  9672  ixxss1  10323  ixxss2  10324  ixxss12  10325  iccss2  10363  rge0ssre  10396  elfzuz  10441  uzdisj  10517  nn0disj  10562  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  0wrd0  11352  modfsummodlemstep  12249  mertenslem2  12328  prmnn  12913  prmuz2  12935  nnmaxpw  12978  sqpweven  12980  2sqpwodd  12981  phimullem  13032  hashgcdlem  13045  1arith  13175  ballotfilem2  13286  ctinfom  13377  ctinf  13379  sgrpmgm  13781  mndsgrp  13793  grpmnd  13871  nsgsubg  14067  ghmgrp1  14107  ghmgrp2  14108  ablgrp  14182  cmnmnd  14194  crngring  14419  rimrhm  14587  subrgring  14641  subrgrcl  14643  rhmpropd  14671  domnnzr  14688  drnglring  14716  flddrngd  14724  2idlelbas  14962  rng2idlsubgsubrng  14966  2idlcpblrng  14969  2idlcpbl  14970  qusrhm  14974  assalmod  15115  assaring  15116  psr1clfi  15198  topontop  15240  tpstop  15261  cntop1  15427  cntop2  15428  hmeocn  15531  isxmet2d  15574  metxmet  15581  xmstps  15683  msxms  15684  xmsxmet  15686  msmet  15687  bdxmet  15727  ivthinclemlr  15863  ivthinclemur  15865  mpodvdsmulf1o  16284  uhgr0vb  16530  trliswlk  16832  eupthfi  16897  eupthistrl  16900  bj-indint  17162  bj-inf2vnlem2  17202  peano4nninf  17255  als-no-surprise  17354