Theorem pm3.26d 321

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 319	. 2 |- ((ps /\ ch) -> ps)
3	1, 2	syl 10	1 |- (ph -> ps)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  pm3.26bi 322  pm3.26bda 420  3simp1 786  euex 1387  elisset 1808  poirr 2836  so 2855  reucl 2875  fcnvres 3633  ndmordi 4037  oneo 4196  ecopoprtrn 4295  eceqopreq 4297  xpmapenlem5 4480  supub 4554  rankel 4652  aceq5lem5 4711  cdafi 4908  nlt1pi 5005  ltbtwnpq 5056  prcdpq 5069  genpcd 5081  1pr 5089  ltexprlem3 5116  ltexprlem4 5117  ltexprlem6 5119  ltaprlem 5122  reclem2pr 5129  reclem3pr 5130  supsrlem1 5197  recnzt 6138  uzwo3lem1 6164  fllet 6176  sqrlem12 6614  replimt 6692  crret 6702  crretOLD 6703  serzrelem 6999  climaddlem3 7052  climmullem2 7057  climmullem3 7058  climmullem4 7059  climmullem5 7060  climmullem8 7063  climabslem 7084  iserzabslem 7114  cvgcmp 7120  cncff 7201  cncffvelrnOLD 7202  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  ege2le3lem1 7269  efcn 7363  addsint 7399  subsint 7400  addcost 7401  subcost 7402  sin01bndlem3 7411  cos01bndlem3 7413  sin01gt0 7418  cos01gt0 7419  acdc2lem2 7431  acdc5lem1 7433  acdc5lem2 7434  uniopnt 7540  msf 7743  metf 7746  metxplem1 7766  metxplem4 7773  metxp 7774  blbas 7812  xplmi 7907  bcthlem11 7943  bcthlem14 7946  bcthlem17 7949  bcthlem18 7950  bcthlem19 7951  bcthlem20 7952  bcthlem21 7953  bcthlem24 7956  bcthlem25 7957  bcthlem26 7958  grplinv 8004  ghgrpilem4 8073  ringsm 8080  ringdi 8083  ringdir 8084  ringass 8085  ringabl 8087  nvvop 8166  isnv 8170  psref 8575  spwval 8582  pilem2 8591  cos2kpi 8608  circcltOLD 8656  hlimseq 8978  shss 9000  shaddclt 9006  shaddcltOLD 9007  projlem26 9127  pjpj0 9170  pjcomp 9536  eighmortht 9804  nmcopexlem5 9870  nmcopexlem6 9871  nmcfnexlem5 9899  nmcfnexlem6 9900  elpjrnt 10027  stclt 10053  hstortht 10057  sthil 10071  ghomfo 10296  ghomid 10299  osbr 10391  filesn 10434  2wsms 10474  doma 10505  coda 10506  ida 10507  dedalg 10520  catded 10541  imonclem 10583  ismonc 10584  icmpmon 10587  iddvvidd 10596  hgradj 10607

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 147  df-an 225

Copyright terms: Public domain