MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancrd Structured version   Unicode version

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
StepHypRef Expression
1 ancrd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 idd 24 . 2  |-  ( ph  ->  ( ps  ->  ps ) )
31, 2jcad 533 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  ps ) ) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator