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  9315  zre  9648  nnssz  9661  ixxss1  10306  ixxss2  10307  ixxss12  10308  iccss2  10346  rge0ssre  10379  elfzuz  10424  uzdisj  10500  nn0disj  10545  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  0wrd0  11330  modfsummodlemstep  12224  mertenslem2  12303  prmnn  12888  prmuz2  12909  oddpwdc  12952  sqpweven  12953  2sqpwodd  12954  phimullem  13003  hashgcdlem  13016  1arith  13146  ballotfilem2  13228  ctinfom  13319  ctinf  13321  sgrpmgm  13722  mndsgrp  13734  grpmnd  13812  nsgsubg  14008  ghmgrp1  14048  ghmgrp2  14049  ablgrp  14092  cmnmnd  14104  crngring  14312  rimrhm  14478  subrgring  14532  subrgrcl  14534  rhmpropd  14562  domnnzr  14579  drnglring  14607  flddrngd  14615  2idlelbas  14853  rng2idlsubgsubrng  14857  2idlcpblrng  14860  2idlcpbl  14861  qusrhm  14865  assalmod  15006  assaring  15007  psr1clfi  15079  topontop  15115  tpstop  15136  cntop1  15302  cntop2  15303  hmeocn  15406  isxmet2d  15449  metxmet  15456  xmstps  15558  msxms  15559  xmsxmet  15561  msmet  15562  bdxmet  15602  ivthinclemlr  15738  ivthinclemur  15740  mpodvdsmulf1o  16104  uhgr0vb  16325  trliswlk  16627  eupthfi  16692  eupthistrl  16695  bj-indint  16957  bj-inf2vnlem2  16997  peano4nninf  17049  als-no-surprise  17147