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  2026  cgsexg  2643  cgsex2g  2644  cgsex4g  2645  reximdva0m  3280  difsn  3543  preq12b  3583  elres  4695  relssres  4697  fnoprabg  5654  1idprl  6878  1idpru  6879  msqge0  7819  mulge0  7822  fzospliti  9298  ialgcvga  10624  prmind2  10693  sqrt2irr  10732