Theorem pm3.27i 261

Description: Inference eliminating a conjunct.

Hypothesis

Ref	Expression
pm3.27i.1	|- (ph /\ ps)

Assertion

Ref	Expression
pm3.27i	|- ps

Proof of Theorem pm3.27i

Step	Hyp	Ref	Expression
1		pm3.27i.1	. 2 |- (ph /\ ps)
2		pm3.27 260	. 2 |- ((ph /\ ps) -> ps)
3	1, 2	ax-mp 6	1 |- ps

Syntax hints:   /\ wa 196

This theorem is referenced by:  ertr 3211  xpmapenlem3 3393  xpmapenlem5 3395  dividt 4256  recrect 4260  crim 4807  climunii 4883  ruclem23 4907  normlem7t 5072  hlimunii 5143  projlem7 5199  omls 5251  shintcl 5294  chintcl 5296  qlaxr3 5529

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