Theorem ancrd 577

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

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  impac  651  equviniva  1960  reupick  3911  prel12  4383  reusv2lem3  4871  ssrelrn  5315  ssrnres  5572  funmo  5904  funssres  5930  dffo4  6375  dffo5  6376  dfwe2  6981  ordpwsuc  7015  ordunisuc2  7044  dfom2  7067  nnsuc  7082  nnaordex  7718  wdom2d  8485  iundom2g  9362  fzospliti  12500  rexuz3  14088  qredeq  15371  prmdvdsfz  15417  dirge  17237  lssssr  18953  lpigen  19256  psgnodpm  19934  neiptopnei  20936  metustexhalf  22361  dyadmbllem  23367  3cyclfrgrrn2  27151  atexch  29240  ordtconnlem1  29970  isbasisrelowllem1  33203  isbasisrelowllem2  33204  phpreu  33393  poimirlem26  33435  sstotbnd3  33575  eqlkr3  34388  dihatexv  36627  dvh3dim2  36737  neik0pk1imk0  38345  pm14.123b  38627  ordpss  38655  climreeq  39845  reuan  41180  2reu1  41186