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  3279  eldifi  3327  elinel1  3391  inss1  3425  sopo  4408  wefr  4453  ordtr  4473  opelxp1  4757  relop  4878  ssrelrn  4920  funmo  5339  funrel  5341  funinsn  5376  fnfun  5424  ffn  5479  f1f  5539  f1of1  5579  f1ofo  5587  isof1o  5943  eqopi  6330  1st2nd2  6333  reldmtpos  6414  swoer  6725  ecopover  6797  ecopoverg  6800  fnfi  7126  casef  7278  nninff  7312  lpowlpo  7358  dfplpq2  7564  enq0ref  7643  cauappcvgprlemopl  7856  cauappcvgprlemdisj  7861  caucvgprlemopl  7879  caucvgprlemdisj  7884  caucvgprprlemopl  7907  caucvgprprlemopu  7909  caucvgprprlemdisj  7912  peano1nnnn  8062  axrnegex  8089  ltxrlt  8235  1nn  9144  zre  9473  nnssz  9486  ixxss1  10129  ixxss2  10130  ixxss12  10131  iccss2  10169  rge0ssre  10202  elfzuz  10246  uzdisj  10318  nn0disj  10363  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  0wrd0  11129  modfsummodlemstep  12008  mertenslem2  12087  prmnn  12672  prmuz2  12693  oddpwdc  12736  sqpweven  12737  2sqpwodd  12738  phimullem  12787  hashgcdlem  12800  1arith  12930  ctinfom  13039  ctinf  13041  sgrpmgm  13480  mndsgrp  13494  grpmnd  13580  nsgsubg  13782  ghmgrp1  13822  ghmgrp2  13823  ablgrp  13866  cmnmnd  13878  crngring  14011  rimrhm  14175  subrgring  14228  subrgrcl  14230  rhmpropd  14258  domnnzr  14274  2idlelbas  14520  rng2idlsubgsubrng  14524  2idlcpblrng  14527  2idlcpbl  14528  qusrhm  14532  psr1clfi  14692  topontop  14728  tpstop  14749  cntop1  14915  cntop2  14916  hmeocn  15019  isxmet2d  15062  metxmet  15069  xmstps  15171  msxms  15172  xmsxmet  15174  msmet  15175  bdxmet  15215  ivthinclemlr  15351  ivthinclemur  15353  mpodvdsmulf1o  15704  uhgr0vb  15925  trliswlk  16181  eupthfi  16246  eupthistrl  16249  bj-indint  16462  bj-inf2vnlem2  16502  peano4nninf  16544