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  954  3simpa  1021  xoror  1424  anxordi  1445  sbidm  1900  reurex  2765  eqimss  3296  eldifi  3345  elinel1  3409  inss1  3445  sopo  4439  wefr  4484  ordtr  4504  opelxp1  4788  relop  4910  ssrelrn  4952  funmo  5372  funrel  5374  funinsn  5410  fnfun  5458  ffn  5513  f1f  5578  f1of1  5618  f1ofo  5626  isof1o  5986  eqopi  6379  1st2nd2  6382  reldmtpos  6497  swoer  6808  ecopover  6880  ecopoverg  6883  fnfi  7216  casef  7392  nninff  7426  lpowlpo  7472  papirr  7575  tapap  7580  dfplpq2  7685  enq0ref  7764  cauappcvgprlemopl  7977  cauappcvgprlemdisj  7982  caucvgprlemopl  8000  caucvgprlemdisj  8005  caucvgprprlemopl  8028  caucvgprprlemopu  8030  caucvgprprlemdisj  8033  peano1nnnn  8183  axrnegex  8210  ltxrlt  8355  1nn  9265  zre  9598  nnssz  9611  ixxss1  10256  ixxss2  10257  ixxss12  10258  iccss2  10296  rge0ssre  10329  elfzuz  10374  uzdisj  10449  nn0disj  10494  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  0wrd0  11275  modfsummodlemstep  12168  mertenslem2  12247  prmnn  12832  prmuz2  12853  oddpwdc  12896  sqpweven  12897  2sqpwodd  12898  phimullem  12947  hashgcdlem  12960  1arith  13090  ballotfilem2  13172  ctinfom  13263  ctinf  13265  sgrpmgm  13670  mndsgrp  13682  grpmnd  13762  nsgsubg  13958  ghmgrp1  13998  ghmgrp2  13999  ablgrp  14042  cmnmnd  14054  crngring  14251  rimrhm  14416  subrgring  14470  subrgrcl  14472  rhmpropd  14500  domnnzr  14517  drnglring  14545  flddrngd  14553  2idlelbas  14790  rng2idlsubgsubrng  14794  2idlcpblrng  14797  2idlcpbl  14798  qusrhm  14802  psr1clfi  14969  topontop  15005  tpstop  15026  cntop1  15192  cntop2  15193  hmeocn  15296  isxmet2d  15339  metxmet  15346  xmstps  15448  msxms  15449  xmsxmet  15451  msmet  15452  bdxmet  15492  ivthinclemlr  15628  ivthinclemur  15630  mpodvdsmulf1o  15984  uhgr0vb  16205  trliswlk  16507  eupthfi  16572  eupthistrl  16575  bj-indint  16827  bj-inf2vnlem2  16867  peano4nninf  16910