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  948  3simpa  997  xoror  1399  anxordi  1420  sbidm  1875  reurex  2725  eqimss  3251  eldifi  3299  elinel1  3363  inss1  3397  sopo  4373  wefr  4418  ordtr  4438  opelxp1  4722  relop  4841  ssrelrn  4883  funmo  5300  funrel  5302  funinsn  5337  fnfun  5385  ffn  5440  f1f  5498  f1of1  5538  f1ofo  5546  isof1o  5894  eqopi  6276  1st2nd2  6279  reldmtpos  6357  swoer  6666  ecopover  6738  ecopoverg  6741  fnfi  7059  casef  7211  nninff  7245  lpowlpo  7291  dfplpq2  7497  enq0ref  7576  cauappcvgprlemopl  7789  cauappcvgprlemdisj  7794  caucvgprlemopl  7812  caucvgprlemdisj  7817  caucvgprprlemopl  7840  caucvgprprlemopu  7842  caucvgprprlemdisj  7845  peano1nnnn  7995  axrnegex  8022  ltxrlt  8168  1nn  9077  zre  9406  nnssz  9419  ixxss1  10056  ixxss2  10057  ixxss12  10058  iccss2  10096  rge0ssre  10129  elfzuz  10173  uzdisj  10245  nn0disj  10290  frecuzrdgtcl  10589  frecuzrdgfunlem  10596  0wrd0  11052  modfsummodlemstep  11853  mertenslem2  11932  prmnn  12517  prmuz2  12538  oddpwdc  12581  sqpweven  12582  2sqpwodd  12583  phimullem  12632  hashgcdlem  12645  1arith  12775  ctinfom  12884  ctinf  12886  sgrpmgm  13324  mndsgrp  13338  grpmnd  13424  nsgsubg  13626  ghmgrp1  13666  ghmgrp2  13667  ablgrp  13710  cmnmnd  13722  crngring  13855  rimrhm  14018  subrgring  14071  subrgrcl  14073  rhmpropd  14101  domnnzr  14117  2idlelbas  14363  rng2idlsubgsubrng  14367  2idlcpblrng  14370  2idlcpbl  14371  qusrhm  14375  psr1clfi  14535  topontop  14571  tpstop  14592  cntop1  14758  cntop2  14759  hmeocn  14862  isxmet2d  14905  metxmet  14912  xmstps  15014  msxms  15015  xmsxmet  15017  msmet  15018  bdxmet  15058  ivthinclemlr  15194  ivthinclemur  15196  mpodvdsmulf1o  15547  uhgr0vb  15765  bj-indint  16036  bj-inf2vnlem2  16076  peano4nninf  16115