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  4458  wefr  4503  ordtr  4523  opelxp1  4808  relop  4930  ssrelrn  4972  funmo  5392  funrel  5394  funinsn  5430  fnfun  5478  ffn  5533  f1f  5598  f1of1  5638  f1ofo  5646  isof1o  6013  eqopi  6406  1st2nd2  6409  reldmtpos  6524  swoer  6835  ecopover  6907  ecopoverg  6910  fnfi  7250  casef  7428  nninff  7462  lpowlpo  7508  papirr  7611  tapap  7616  dfplpq2  7721  enq0ref  7800  cauappcvgprlemopl  8013  cauappcvgprlemdisj  8018  caucvgprlemopl  8036  caucvgprlemdisj  8041  caucvgprprlemopl  8064  caucvgprprlemopu  8066  caucvgprprlemdisj  8069  peano1nnnn  8219  axrnegex  8246  ltxrlt  8391  1nn  9317  zre  9652  nnssz  9665  ixxss1  10316  ixxss2  10317  ixxss12  10318  iccss2  10356  rge0ssre  10389  elfzuz  10434  uzdisj  10510  nn0disj  10555  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  0wrd0  11344  modfsummodlemstep  12240  mertenslem2  12319  prmnn  12904  prmuz2  12926  nnmaxpw  12969  sqpweven  12971  2sqpwodd  12972  phimullem  13023  hashgcdlem  13036  1arith  13166  ballotfilem2  13277  ctinfom  13368  ctinf  13370  sgrpmgm  13771  mndsgrp  13783  grpmnd  13861  nsgsubg  14057  ghmgrp1  14097  ghmgrp2  14098  ablgrp  14141  cmnmnd  14153  crngring  14361  rimrhm  14527  subrgring  14581  subrgrcl  14583  rhmpropd  14611  domnnzr  14628  drnglring  14656  flddrngd  14664  2idlelbas  14902  rng2idlsubgsubrng  14906  2idlcpblrng  14909  2idlcpbl  14910  qusrhm  14914  assalmod  15055  assaring  15056  psr1clfi  15128  topontop  15164  tpstop  15185  cntop1  15351  cntop2  15352  hmeocn  15455  isxmet2d  15498  metxmet  15505  xmstps  15607  msxms  15608  xmsxmet  15610  msmet  15611  bdxmet  15651  ivthinclemlr  15787  ivthinclemur  15789  mpodvdsmulf1o  16185  uhgr0vb  16423  trliswlk  16725  eupthfi  16790  eupthistrl  16793  bj-indint  17055  bj-inf2vnlem2  17095  peano4nninf  17147  als-no-surprise  17245