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  589  pm5.62dc  951  3simpa  1018  xoror  1421  anxordi  1442  sbidm  1897  reurex  2750  eqimss  3278  eldifi  3326  elinel1  3390  inss1  3424  sopo  4403  wefr  4448  ordtr  4468  opelxp1  4752  relop  4871  ssrelrn  4913  funmo  5332  funrel  5334  funinsn  5369  fnfun  5417  ffn  5472  f1f  5530  f1of1  5570  f1ofo  5578  isof1o  5930  eqopi  6316  1st2nd2  6319  reldmtpos  6397  swoer  6706  ecopover  6778  ecopoverg  6781  fnfi  7099  casef  7251  nninff  7285  lpowlpo  7331  dfplpq2  7537  enq0ref  7616  cauappcvgprlemopl  7829  cauappcvgprlemdisj  7834  caucvgprlemopl  7852  caucvgprlemdisj  7857  caucvgprprlemopl  7880  caucvgprprlemopu  7882  caucvgprprlemdisj  7885  peano1nnnn  8035  axrnegex  8062  ltxrlt  8208  1nn  9117  zre  9446  nnssz  9459  ixxss1  10096  ixxss2  10097  ixxss12  10098  iccss2  10136  rge0ssre  10169  elfzuz  10213  uzdisj  10285  nn0disj  10330  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  0wrd0  11092  modfsummodlemstep  11963  mertenslem2  12042  prmnn  12627  prmuz2  12648  oddpwdc  12691  sqpweven  12692  2sqpwodd  12693  phimullem  12742  hashgcdlem  12755  1arith  12885  ctinfom  12994  ctinf  12996  sgrpmgm  13435  mndsgrp  13449  grpmnd  13535  nsgsubg  13737  ghmgrp1  13777  ghmgrp2  13778  ablgrp  13821  cmnmnd  13833  crngring  13966  rimrhm  14129  subrgring  14182  subrgrcl  14184  rhmpropd  14212  domnnzr  14228  2idlelbas  14474  rng2idlsubgsubrng  14478  2idlcpblrng  14481  2idlcpbl  14482  qusrhm  14486  psr1clfi  14646  topontop  14682  tpstop  14703  cntop1  14869  cntop2  14870  hmeocn  14973  isxmet2d  15016  metxmet  15023  xmstps  15125  msxms  15126  xmsxmet  15128  msmet  15129  bdxmet  15169  ivthinclemlr  15305  ivthinclemur  15307  mpodvdsmulf1o  15658  uhgr0vb  15878  bj-indint  16252  bj-inf2vnlem2  16292  peano4nninf  16331