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  1741  euanOLD  2332  2eu1OLD  2365  reupick  3639  prel12  4054  reusv2lem3  4500  ssrnres  5281  funmo  5439  funssres  5463  dffo4  5864  dffo5  5865  dfwe2  6398  ordpwsuc  6431  ordunisuc2  6460  dfom2  6483  nnsuc  6498  nnaordex  7082  wdom2d  7800  iundom2g  8709  fzospliti  11586  rexuz3  12841  qredeq  13797  dirge  15412  lssssr  17039  lpigen  17343  psgnodpm  18023  neiptopnei  18741  metustexhalfOLD  20143  metustexhalf  20144  dyadmbllem  21084  atexch  25790  ordtconlem1  26359  sstotbnd3  28680  pm14.123b  29685  ordpss  29712  climreeq  29791  reuan  30009  2reu1  30015  hash2sspr  30232  3cyclfrgrarn2  30611  eqlkr3  32751  dihatexv  34988  dvh3dim2  35098