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 1168  pwpw0 2469  sssn 2473  pwsnALT 2501  opprc3 2797  tfis 3127  oeordi 4214  unblem3 4542  trcl 4645  rankr1 4674  ac5b 4753  sqr2irr 6729  metelcls 7965  h1datom 9504

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