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  2097  cgsexg  2761  cgsex2g  2762  cgsex4g  2763  reximdva0m  3424  difsn  3710  preq12b  3750  elres  4920  relssres  4922  fnoprabg  5943  1idprl  7531  1idpru  7532  msqge0  8514  mulge0  8517  fzospliti  10111  algcvga  11983  prmind2  12052  sqrt2irr  12094  metrest  13146  2sqlem10  13601