Theorem ancld 325

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 307	1 |- ( ph -> ( ps -> ( ps /\ ch ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mopick2  2170  cgsexg  2857  cgsex2g  2858  cgsex4g  2859  reximdva0m  3537  difsn  3852  preq12b  3895  elres  5101  relssres  5103  fnoprabg  6192  1idprl  7963  1idpru  7964  msqge0  8952  mulge0  8955  fzospliti  10602  algcvga  12854  prmind2  12923  sqrt2irr  12966  grpinveu  13902  metrest  15732  chtqub  16296  2sqlem10  16449  clwwlkn1loopb  16866