Theorem anc2li 324

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

Syntax hints:   -> wi 3   /\ wa 239

This theorem is referenced by:  imdistani 489  equvini 1369  equviniOLD 1370  pwpw0 2956  sssn 2964  pwsnALT 2995  opprc3 3358  ordtr2 3523  tfis 3749  oeordi 5073  unblem3 5445  trcl 5561  rankr1 5594  ac5b 5711  sqr2irr 7774  metelcls 9038  h1datomi 10929  wfisg 13709  frinsg 13733  sbiota1 16081

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 163  df-an 241

Copyright terms: Public domain