Theorem pm3.26d 328

Description: Deduction eliminating a conjunct.

Hypothesis

Ref	Expression
pm3.26d.1	|- (ph -> (ps /\ ch))

Assertion

Ref	Expression
pm3.26d	|- (ph -> ps)

Proof of Theorem pm3.26d

Step	Hyp	Ref	Expression
1		pm3.26d.1	. 2 |- (ph -> (ps /\ ch))
2		pm3.26 326	. 2 |- ((ps /\ ch) -> ps)
3	1, 2	syl 10	1 |- (ph -> ps)

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  pm3.26bi 329  pm3.26bda 429  3simp1 800  euex 1436  elisset 1864  poirr 2901  so 2920  reucl 2942  fcnvres 3705  ndmordi 4109  oneo 4270  ecopoprtrn 4372  eceqopreq 4374  xpmapenlem5 4565  supub 4640  rankel 4742  aceq5lem5 4801  cdafi 5001  nlt1pi 5098  ltbtwnpq 5149  prcdpq 5162  genpcd 5174  1pr 5182  ltexprlem3 5209  ltexprlem4 5210  ltexprlem6 5212  ltaprlem 5215  reclem2pr 5222  reclem3pr 5223  supsrlem1 5290  recnz 6276  uzwo3lem1 6301  flle 6340  sqrlem12 6774  replim 6851  crre 6859  serzrelem 7151  climaddlem3 7206  climmullem2 7211  climmullem3 7212  climmullem4 7213  climmullem5 7214  climmullem8 7217  climabslem 7238  iserzabslem 7268  cvgcmpi 7274  cncff 7356  cncffvelrnOLD 7357  ivthlem6 7376  ivthlem7 7377  ege2le3lem1 7417  efcn 7514  addsin 7548  subsin 7549  addcos 7550  subcos 7551  sin01bndlem3 7561  cos01bndlem3 7563  sin01gt0 7568  cos01gt0 7569  acdc2lem2 7581  acdc5lem1 7583  acdc5lem2 7584  uniopn 7689  msf 7889  metf 7892  metxplem1 7911  metxplem4 7918  metxp 7919  blbas 7957  xplmi 8058  bcthlem11 8094  bcthlem14 8097  bcthlem17 8100  bcthlem18 8101  bcthlem19 8102  bcthlem20 8103  bcthlem21 8104  bcthlem24 8107  bcthlem25 8108  bcthlem26 8109  grplinv 8154  ghgrpilem4 8220  ringsm 8227  ringdi 8230  ringdir 8231  ringass 8232  ringabl 8234  nvvop 8312  isnv 8315  psref 8733  spwval 8743  spwnex 8745  pilem2 8755  cos2kpi 8772  hlimseqi 9140  shss 9162  shaddcl 9168  shaddclOLD 9169  projlem26 9294  pjpj0i 9338  pjcompi 9702  eighmorth 9971  nmcopexlem5 10038  nmcopexlem6 10039  nmcfnexlem5 10067  nmcfnexlem6 10068  elpjrn 10201  stcl 10227  hstorth 10231  sthil 10245  ghomfo 10476  ghomid 10479  osbr 10598  filesn 10653  2wsms 10712  doma 10743  coda 10744  ida 10745  dedalg 10758  catded 10779  imonclem 10823  ismonc 10824  icmpmon 10826  iddvvidd 10842  hgradj 10855

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 154  df-an 232

Copyright terms: Public domain