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  953  3simpa  1020  xoror  1423  anxordi  1444  sbidm  1899  reurex  2752  eqimss  3281  eldifi  3329  elinel1  3393  inss1  3427  sopo  4410  wefr  4455  ordtr  4475  opelxp1  4759  relop  4880  ssrelrn  4922  funmo  5341  funrel  5343  funinsn  5379  fnfun  5427  ffn  5482  f1f  5542  f1of1  5582  f1ofo  5590  isof1o  5947  eqopi  6334  1st2nd2  6337  reldmtpos  6418  swoer  6729  ecopover  6801  ecopoverg  6804  fnfi  7134  casef  7286  nninff  7320  lpowlpo  7366  dfplpq2  7573  enq0ref  7652  cauappcvgprlemopl  7865  cauappcvgprlemdisj  7870  caucvgprlemopl  7888  caucvgprlemdisj  7893  caucvgprprlemopl  7916  caucvgprprlemopu  7918  caucvgprprlemdisj  7921  peano1nnnn  8071  axrnegex  8098  ltxrlt  8244  1nn  9153  zre  9482  nnssz  9495  ixxss1  10138  ixxss2  10139  ixxss12  10140  iccss2  10178  rge0ssre  10211  elfzuz  10255  uzdisj  10327  nn0disj  10372  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  0wrd0  11138  modfsummodlemstep  12017  mertenslem2  12096  prmnn  12681  prmuz2  12702  oddpwdc  12745  sqpweven  12746  2sqpwodd  12747  phimullem  12796  hashgcdlem  12809  1arith  12939  ctinfom  13048  ctinf  13050  sgrpmgm  13489  mndsgrp  13503  grpmnd  13589  nsgsubg  13791  ghmgrp1  13831  ghmgrp2  13832  ablgrp  13875  cmnmnd  13887  crngring  14020  rimrhm  14184  subrgring  14237  subrgrcl  14239  rhmpropd  14267  domnnzr  14283  2idlelbas  14529  rng2idlsubgsubrng  14533  2idlcpblrng  14536  2idlcpbl  14537  qusrhm  14541  psr1clfi  14701  topontop  14737  tpstop  14758  cntop1  14924  cntop2  14925  hmeocn  15028  isxmet2d  15071  metxmet  15078  xmstps  15180  msxms  15181  xmsxmet  15183  msmet  15184  bdxmet  15224  ivthinclemlr  15360  ivthinclemur  15362  mpodvdsmulf1o  15713  uhgr0vb  15934  trliswlk  16236  eupthfi  16301  eupthistrl  16304  bj-indint  16526  bj-inf2vnlem2  16566  peano4nninf  16608