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  595  pm5.62dc  958  3simpa  1025  xoror  1428  anxordi  1449  sbidm  1904  reurex  2771  eqimss  3302  eldifi  3351  elinel1  3415  inss1  3451  sopo  4453  wefr  4498  ordtr  4518  opelxp1  4803  relop  4925  ssrelrn  4967  funmo  5387  funrel  5389  funinsn  5425  fnfun  5473  ffn  5528  f1f  5593  f1of1  5633  f1ofo  5641  isof1o  6003  eqopi  6396  1st2nd2  6399  reldmtpos  6514  swoer  6825  ecopover  6897  ecopoverg  6900  fnfi  7240  casef  7418  nninff  7452  lpowlpo  7498  papirr  7601  tapap  7606  dfplpq2  7711  enq0ref  7790  cauappcvgprlemopl  8003  cauappcvgprlemdisj  8008  caucvgprlemopl  8026  caucvgprlemdisj  8031  caucvgprprlemopl  8054  caucvgprprlemopu  8056  caucvgprprlemdisj  8059  peano1nnnn  8209  axrnegex  8236  ltxrlt  8381  1nn  9294  zre  9627  nnssz  9640  ixxss1  10285  ixxss2  10286  ixxss12  10287  iccss2  10325  rge0ssre  10358  elfzuz  10403  uzdisj  10478  nn0disj  10523  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  0wrd0  11308  modfsummodlemstep  12202  mertenslem2  12281  prmnn  12866  prmuz2  12887  oddpwdc  12930  sqpweven  12931  2sqpwodd  12932  phimullem  12981  hashgcdlem  12994  1arith  13124  ballotfilem2  13206  ctinfom  13297  ctinf  13299  sgrpmgm  13699  mndsgrp  13711  grpmnd  13789  nsgsubg  13985  ghmgrp1  14025  ghmgrp2  14026  ablgrp  14069  cmnmnd  14081  crngring  14286  rimrhm  14451  subrgring  14505  subrgrcl  14507  rhmpropd  14535  domnnzr  14552  drnglring  14580  flddrngd  14588  2idlelbas  14825  rng2idlsubgsubrng  14829  2idlcpblrng  14832  2idlcpbl  14833  qusrhm  14837  psr1clfi  15002  topontop  15038  tpstop  15059  cntop1  15225  cntop2  15226  hmeocn  15329  isxmet2d  15372  metxmet  15379  xmstps  15481  msxms  15482  xmsxmet  15484  msmet  15485  bdxmet  15525  ivthinclemlr  15661  ivthinclemur  15663  mpodvdsmulf1o  16018  uhgr0vb  16239  trliswlk  16541  eupthfi  16606  eupthistrl  16609  bj-indint  16871  bj-inf2vnlem2  16911  peano4nninf  16954