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 1164  pwpw0 2460  sssn 2464  opprc3 2787  tfis 3117  oeordi 4198  unblem3 4519  trcl 4617  rankr1 4646  ac5b 4725  sqr2irr 6659  metelcls 7900  h1datom 9421

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