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  2170  cgsexg  2857  cgsex2g  2858  cgsex4g  2859  reximdva0m  3537  difsn  3847  preq12b  3890  elres  5094  relssres  5096  fnoprabg  6179  1idprl  7947  1idpru  7948  msqge0  8934  mulge0  8937  fzospliti  10563  algcvga  12807  prmind2  12876  sqrt2irr  12918  grpinveu  13820  metrest  15530  2sqlem10  16158  clwwlkn1loopb  16575