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  2139  cgsexg  2812  cgsex2g  2813  cgsex4g  2814  reximdva0m  3484  difsn  3781  preq12b  3824  elres  5014  relssres  5016  fnoprabg  6069  1idprl  7738  1idpru  7739  msqge0  8724  mulge0  8727  fzospliti  10335  algcvga  12488  prmind2  12557  sqrt2irr  12599  grpinveu  13485  metrest  15093  2sqlem10  15717