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  2200  2eu1  2223  reupick  3452  prel12  3789  reusv2lem3  4537  dfwe2  4573  ordpwsuc  4606  ordunisuc2  4635  dfom2  4658  nnsuc  4673  ssrnres  5116  funmo  5271  funssres  5294  dffo4  5676  dffo5  5677  nnaordex  6636  wdom2d  7294  iundom2g  8162  lbinfm  9707  fzospliti  10898  rexuz3  11832  qredeq  12785  dirge  14359  lssssr  15710  lpigen  16008  dyadmbllem  18954  atexch  22961  iepiclem  25823  sstotbnd3  26500  pm14.123b  27626  ordpss  27654  climreeq  27739  reuan  27958  2reu1  27964  eqlkr3  29291  dihatexv  31528  dvh3dim2  31638
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