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  2080  cgsexg  2716  cgsex2g  2717  cgsex4g  2718  reximdva0m  3373  difsn  3652  preq12b  3692  elres  4850  relssres  4852  fnoprabg  5865  1idprl  7391  1idpru  7392  msqge0  8371  mulge0  8374  fzospliti  9946  algcvga  11721  prmind2  11790  sqrt2irr  11829  metrest  12664