Theorem ancld 323

Description: Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)

Hypothesis

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

Assertion

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

Proof of Theorem ancld

Step	Hyp	Ref	Expression
1		idd 21	. 2 |- ( ph -> ( ps -> ps ) )
2		ancld.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	jcad 305	1 |- ( ph -> ( ps -> ( ps /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  mopick2  2083  cgsexg  2724  cgsex2g  2725  cgsex4g  2726  reximdva0m  3383  difsn  3665  preq12b  3705  elres  4863  relssres  4865  fnoprabg  5880  1idprl  7422  1idpru  7423  msqge0  8402  mulge0  8405  fzospliti  9984  algcvga  11768  prmind2  11837  sqrt2irr  11876  metrest  12714