Theorem ancld 318

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 301	1 |- ( ph -> ( ps -> ( ps /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106

This theorem is referenced by:  mopick2  2024  cgsexg  2634  cgsex2g  2635  cgsex4g  2636  reximdva0m  3263  difsn  3523  preq12b  3562  elres  4664  relssres  4666  fnoprabg  5622  1idprl  6780  1idpru  6781  msqge0  7716  mulge0  7719  fzospliti  9185  ialgcvga  10433  prmind2  10502  sqrt2irr  10541