Theorem anc2li 250

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

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  imdistani 340  eqvin.l1 851  sssn 1852  pwpw0 1883  opprc3 1908  tfis 2245  unblem3 3433  trcl 3489  rankr1 3518  ac5b 3574  nn2get 4438  sqr2irr 4782  h1datom 5483

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org