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  6111  1idprl  7788  1idpru  7789  msqge0  8774  mulge0  8777  fzospliti  10386  algcvga  12589  prmind2  12658  sqrt2irr  12700  grpinveu  13587  metrest  15196  2sqlem10  15820  clwwlkn1loopb  16162