Theorem pm3.26d 258

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

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  pm3.26bd 259  3simp1 594  euex 1021  elisset 1354  reucl 1957  poirr 2133  so 2152  supub 2160  dmexg 2551  fcnvres 2768  ndmordi 3065  ecopoprtrn 3247  eceqopreq 3249  xpmapenlem5 3395  rankel 3524  aceq5lem5 3562  cdafi 3730  nlt1pi 3827  ltbtwnpq 3878  prn0 3887  prcdpq 3891  genpcd 3903  1pr 3911  ltexprlem3 3938  ltexprlem4 3939  ltexprlem6 3941  ltaprlem 3944  reclem2pr 3951  reclem3pr 3952  supsrlem1 4019  uzwo3lem1 4614  flgzt 4626  flidt 4627  sqrlem12 4742  replimt 4798  climseq 4878  hlimseq 5109  shss 5117  projlem26 5218  pjpj0 5259  pjcomp 5565  stclt 5672  sthil 5675

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org