Theorem pm3.26i 257

Description: Inference eliminating a conjunct.

Hypothesis

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

Assertion

Ref	Expression
pm3.26i	|- ph

Proof of Theorem pm3.26i

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

Syntax hints:   /\ wa 196

This theorem is referenced by:  ssid 1519  ersym 3209  ssdomg 3311  xpmapenlem3 3393  xpmapenlem5 3395  ssrankr1 3520  dividt 4256  recrect 4260  crre 4806  climunii 4883  infunabs 4946  infcdaabs 4947  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