Theorem ancrd 247

Description: Deduction conjoining antecedent to right of consequent in nested implication.

Hypothesis

Ref	Expression
ancrd.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
ancrd	|- (ph -> (ps -> (ch /\ ps)))

Proof of Theorem ancrd

Step	Hyp	Ref	Expression
1		ancrd.1	. 2 |- (ph -> (ps -> ch))
2		ancr 243	. 2 |- ((ps -> ch) -> (ps -> (ch /\ ps)))
3	1, 2	syl 12	1 |- (ph -> (ps -> (ch /\ ps)))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  impac 304  2eu1 1067  reupick 1578  prel12 1875  dfwe2 2187  onpwsuc 2315  dfom2 2374  nnsuc 2389  funssres 2698  f1fv 2916  ltexpq2 3875  ltexpri 3943  suplem1pr 3955  replimt 4798  atexch 5769

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