Theorem anc2li 309

Description: Deduction conjoining antecedent to left of consequent in nested implication.

Hypothesis

Ref	Expression
anc2li.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
anc2li	|- (ph -> (ps -> (ph /\ ch)))

Proof of Theorem anc2li

Step	Hyp	Ref	Expression
1		anc2li.1	. 2 |- (ph -> (ps -> ch))
2		anc2l 307	. 2 |- ((ph -> (ps -> ch)) -> (ph -> (ps -> (ph /\ ch))))
3	1, 2	ax-mp 7	1 |- (ph -> (ps -> (ph /\ ch)))

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  imdistani 454  equvini 1210  pwpw0 2523  sssn 2527  pwsnALT 2555  opprc3 2853  tfis 3184  oeordi 4272  unblem3 4605  trcl 4707  rankr1 4736  ac5b 4815  sqr2irr 6819  metelcls 8050  h1datomi 9587

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 154  df-an 232

Copyright terms: Public domain