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  2137  cgsexg  2807  cgsex2g  2808  cgsex4g  2809  reximdva0m  3476  difsn  3770  preq12b  3811  elres  4995  relssres  4997  fnoprabg  6046  1idprl  7703  1idpru  7704  msqge0  8689  mulge0  8692  fzospliti  10300  algcvga  12373  prmind2  12442  sqrt2irr  12484  grpinveu  13370  metrest  14978  2sqlem10  15602