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 ) ) )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  mopick2  2163  cgsexg  2839  cgsex2g  2840  cgsex4g  2841  reximdva0m  3512  difsn  3815  preq12b  3858  elres  5055  relssres  5057  fnoprabg  6132  1idprl  7870  1idpru  7871  msqge0  8855  mulge0  8858  fzospliti  10475  algcvga  12703  prmind2  12772  sqrt2irr  12814  grpinveu  13701  metrest  15317  2sqlem10  15944  clwwlkn1loopb  16361