Theorem ancr 319

Description: Conjoin antecedent to right of consequent.

Assertion

Ref	Expression
ancr	|- ((ph -> ps) -> (ph -> (ps /\ ph)))

Proof of Theorem ancr

Step	Hyp	Ref	Expression
1		pm3.21 306	. 2 |- (ph -> (ps -> (ps /\ ph)))
2	1	a2i 10	1 |- ((ph -> ps) -> (ph -> (ps /\ ph)))

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  ancrd 323  ancrb 357  intmin4 3246  chsscmi 10745  bnj1098 12917  bnj1171 13439  lukshef-ax2 14239  pm14.122b 16387

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 164  df-an 242

Copyright terms: Public domain