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  2109  cgsexg  2774  cgsex2g  2775  cgsex4g  2776  reximdva0m  3440  difsn  3731  preq12b  3772  elres  4945  relssres  4947  fnoprabg  5979  1idprl  7592  1idpru  7593  msqge0  8576  mulge0  8579  fzospliti  10179  algcvga  12054  prmind2  12123  sqrt2irr  12165  grpinveu  12917  metrest  14146  2sqlem10  14612