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  2109  cgsexg  2773  cgsex2g  2774  cgsex4g  2775  reximdva0m  3439  difsn  3730  preq12b  3771  elres  4944  relssres  4946  fnoprabg  5976  1idprl  7589  1idpru  7590  msqge0  8573  mulge0  8576  fzospliti  10176  algcvga  12051  prmind2  12120  sqrt2irr  12162  grpinveu  12911  metrest  14009  2sqlem10  14475