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  2163  cgsexg  2838  cgsex2g  2839  cgsex4g  2840  reximdva0m  3510  difsn  3810  preq12b  3853  elres  5049  relssres  5051  fnoprabg  6122  1idprl  7810  1idpru  7811  msqge0  8796  mulge0  8799  fzospliti  10413  algcvga  12641  prmind2  12710  sqrt2irr  12752  grpinveu  13639  metrest  15249  2sqlem10  15873  clwwlkn1loopb  16290