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

Theorem ancrd 537
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 21 . 2  |-  ( ph  ->  ( ps  ->  ps ) )
31, 2jcad 519 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  impac  604  euan  2213  2eu1  2236  reupick  3465  prel12  3805  reusv2lem3  4553  dfwe2  4589  ordpwsuc  4622  ordunisuc2  4651  dfom2  4674  nnsuc  4689  ssrnres  5132  funmo  5287  funssres  5310  dffo4  5692  dffo5  5693  nnaordex  6652  wdom2d  7310  iundom2g  8178  lbinfm  9723  fzospliti  10914  rexuz3  11848  qredeq  12801  dirge  14375  lssssr  15726  lpigen  16024  dyadmbllem  18970  atexch  22977  iepiclem  25926  sstotbnd3  26603  pm14.123b  27729  ordpss  27757  climreeq  27842  reuan  28061  2reu1  28067  eqlkr3  29913  dihatexv  32150  dvh3dim2  32260
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator