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  5099  relssres  5101  fnoprabg  6189  1idprl  7958  1idpru  7959  msqge0  8947  mulge0  8950  fzospliti  10596  algcvga  12848  prmind2  12917  sqrt2irr  12960  grpinveu  13896  metrest  15698  chtqub  16257  2sqlem10  16410  clwwlkn1loopb  16827