Theorem ancld 323

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 305	1 |- ( ph -> ( ps -> ( ps /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mopick2  2102  cgsexg  2765  cgsex2g  2766  cgsex4g  2767  reximdva0m  3430  difsn  3717  preq12b  3757  elres  4927  relssres  4929  fnoprabg  5954  1idprl  7552  1idpru  7553  msqge0  8535  mulge0  8538  fzospliti  10132  algcvga  12005  prmind2  12074  sqrt2irr  12116  grpinveu  12741  metrest  13300  2sqlem10  13755