Theorem ancrd 561

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 25	. 2 |- ( ph -> ( ps -> ps ) )
3	1, 2	jcad 540	1 |- ( ph -> ( ps -> ( ch /\ ps ) ) )

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  impac  631  equviniv  1883  reupick  3739  prel12  4165  reusv2lem3  4623  ssrnres  5297  funmo  5621  funssres  5645  dffo4  6066  dffo5  6067  dfwe2  6640  ordpwsuc  6674  ordunisuc2  6703  dfom2  6726  nnsuc  6741  nnaordex  7370  wdom2d  8126  iundom2g  8996  fzospliti  11987  rexuz3  13466  prmdvdsfz  14704  qredeq  14718  dirge  16538  lssssr  18231  lpigen  18535  psgnodpm  19211  neiptopnei  20203  metustexhalf  21626  dyadmbllem  22613  3cyclfrgrarn2  25798  atexch  28090  ordtconlem1  28781  isbasisrelowllem1  31804  isbasisrelowllem2  31805  phpreu  31975  poimirlem26  32012  sstotbnd3  32154  eqlkr3  32713  dihatexv  34952  dvh3dim2  35062  pm14.123b  36822  ordpss  36849  climreeq  37779  reuan  38736  2reu1  38742  ssrelrn  39148