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  7429  nninff  7463  lpowlpo  7509  papirr  7612  tapap  7617  dfplpq2  7722  enq0ref  7801  cauappcvgprlemopl  8014  cauappcvgprlemdisj  8019  caucvgprlemopl  8037  caucvgprlemdisj  8042  caucvgprprlemopl  8065  caucvgprprlemopu  8067  caucvgprprlemdisj  8070  peano1nnnn  8220  axrnegex  8247  ltxrlt  8392  1nn  9318  zre  9653  nnssz  9666  ixxss1  10317  ixxss2  10318  ixxss12  10319  iccss2  10357  rge0ssre  10390  elfzuz  10435  uzdisj  10511  nn0disj  10556  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  0wrd0  11346  modfsummodlemstep  12243  mertenslem2  12322  prmnn  12907  prmuz2  12929  nnmaxpw  12972  sqpweven  12974  2sqpwodd  12975  phimullem  13026  hashgcdlem  13039  1arith  13169  ballotfilem2  13280  ctinfom  13371  ctinf  13373  sgrpmgm  13775  mndsgrp  13787  grpmnd  13865  nsgsubg  14061  ghmgrp1  14101  ghmgrp2  14102  ablgrp  14176  cmnmnd  14188  crngring  14396  rimrhm  14562  subrgring  14616  subrgrcl  14618  rhmpropd  14646  domnnzr  14663  drnglring  14691  flddrngd  14699  2idlelbas  14937  rng2idlsubgsubrng  14941  2idlcpblrng  14944  2idlcpbl  14945  qusrhm  14949  assalmod  15090  assaring  15091  psr1clfi  15170  topontop  15206  tpstop  15227  cntop1  15393  cntop2  15394  hmeocn  15497  isxmet2d  15540  metxmet  15547  xmstps  15649  msxms  15650  xmsxmet  15652  msmet  15653  bdxmet  15693  ivthinclemlr  15829  ivthinclemur  15831  mpodvdsmulf1o  16245  uhgr0vb  16491  trliswlk  16793  eupthfi  16858  eupthistrl  16861  bj-indint  17123  bj-inf2vnlem2  17163  peano4nninf  17215  als-no-surprise  17314