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  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
  Copyright terms: Public domain W3C validator