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  2161  cgsexg  2835  cgsex2g  2836  cgsex4g  2837  reximdva0m  3507  difsn  3805  preq12b  3848  elres  5041  relssres  5043  fnoprabg  6105  1idprl  7777  1idpru  7778  msqge0  8763  mulge0  8766  fzospliti  10374  algcvga  12573  prmind2  12642  sqrt2irr  12684  grpinveu  13571  metrest  15180  2sqlem10  15804