Theorem anc2li 302

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 300	. 2 |- ((ph -> (ps -> ch)) -> (ph -> (ps -> (ph /\ ch))))
3	1, 2	ax-mp 7	1 |- (ph -> (ps -> (ph /\ ch)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  imdistani 443  equvini 1151  pwpw0 2439  sssn 2443  opprc3 2764  tfis 3090  oeordi 4152  unblem3 4471  trcl 4569  rankr1 4598  ac5b 4677  sqr2irr 6610  metelcls 7848  h1datom 9635

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 147  df-an 225

Copyright terms: Public domain