Theorem ancrd 554

Description: Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)

Hypothesis

Ref	Expression
ancrd.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
ancrd	|- ( ph -> ( ps -> ( ch /\ ps ) ) )

Proof of Theorem ancrd

Step	Hyp	Ref	Expression
1		ancrd.1	. 2 |- ( ph -> ( ps -> ch ) )
2		idd 24	. 2 |- ( ph -> ( ps -> ps ) )
3	1, 2	jcad 533	1 |- ( ph -> ( ps -> ( ch /\ ps ) ) )

Syntax hints:   -> wi 4   /\ wa 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  impac  621  equviniv  1752  euanOLD  2354  2eu1OLD  2387  reupick  3787  prel12  4209  reusv2lem3  4656  ssrnres  5451  funmo  5610  funssres  5634  dffo4  6048  dffo5  6049  dfwe2  6612  ordpwsuc  6645  ordunisuc2  6674  dfom2  6697  nnsuc  6712  nnaordex  7299  wdom2d  8018  iundom2g  8927  fzospliti  11837  hash2sspr  12507  rexuz3  13161  qredeq  14123  dirge  15741  lssssr  17470  lpigen  17774  psgnodpm  18493  neiptopnei  19501  metustexhalfOLD  20934  metustexhalf  20935  dyadmbllem  21876  3cyclfrgrarn2  24837  atexch  27123  ordtconlem1  27731  sstotbnd3  30199  pm14.123b  31235  ordpss  31262  climreeq  31478  reuan  31975  2reu1  31981  eqlkr3  34299  dihatexv  36536  dvh3dim2  36646