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:  pm5.62dc  947  3simpa  996  xoror  1390  anxordi  1411  sbidm  1865  reurex  2715  eqimss  3238  eldifi  3286  elinel1  3350  inss1  3384  sopo  4349  wefr  4394  ordtr  4414  opelxp1  4698  relop  4817  funmo  5274  funrel  5276  funinsn  5308  fnfun  5356  ffn  5410  f1f  5466  f1of1  5506  f1ofo  5514  isof1o  5857  eqopi  6239  1st2nd2  6242  reldmtpos  6320  swoer  6629  ecopover  6701  ecopoverg  6704  fnfi  7011  casef  7163  nninff  7197  lpowlpo  7243  dfplpq2  7440  enq0ref  7519  cauappcvgprlemopl  7732  cauappcvgprlemdisj  7737  caucvgprlemopl  7755  caucvgprlemdisj  7760  caucvgprprlemopl  7783  caucvgprprlemopu  7785  caucvgprprlemdisj  7788  peano1nnnn  7938  axrnegex  7965  ltxrlt  8111  1nn  9020  zre  9349  nnssz  9362  ixxss1  9998  ixxss2  9999  ixxss12  10000  iccss2  10038  rge0ssre  10071  elfzuz  10115  uzdisj  10187  nn0disj  10232  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  0wrd0  10980  modfsummodlemstep  11641  mertenslem2  11720  prmnn  12305  prmuz2  12326  oddpwdc  12369  sqpweven  12370  2sqpwodd  12371  phimullem  12420  hashgcdlem  12433  1arith  12563  ctinfom  12672  ctinf  12674  sgrpmgm  13111  mndsgrp  13125  grpmnd  13211  nsgsubg  13413  ghmgrp1  13453  ghmgrp2  13454  ablgrp  13497  cmnmnd  13509  crngring  13642  rimrhm  13805  subrgring  13858  subrgrcl  13860  rhmpropd  13888  domnnzr  13904  2idlelbas  14150  rng2idlsubgsubrng  14154  2idlcpblrng  14157  2idlcpbl  14158  qusrhm  14162  psr1clfi  14322  topontop  14358  tpstop  14379  cntop1  14545  cntop2  14546  hmeocn  14649  isxmet2d  14692  metxmet  14699  xmstps  14801  msxms  14802  xmsxmet  14804  msmet  14805  bdxmet  14845  ivthinclemlr  14981  ivthinclemur  14983  mpodvdsmulf1o  15334  bj-indint  15685  bj-inf2vnlem2  15725  peano4nninf  15761