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

Theorem ancrd 538
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 22 . 2  |-  ( ph  ->  ( ps  ->  ps ) )
31, 2jcad 520 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  impac  605  euan  2338  2eu1  2361  reupick  3625  prel12  3975  reusv2lem3  4726  dfwe2  4762  ordpwsuc  4795  ordunisuc2  4824  dfom2  4847  nnsuc  4862  ssrnres  5309  funmo  5470  funssres  5493  dffo4  5885  dffo5  5886  nnaordex  6881  wdom2d  7548  iundom2g  8415  fzospliti  11165  rexuz3  12152  qredeq  13106  dirge  14682  lssssr  16029  lpigen  16327  neiptopnei  17196  metustexhalfOLD  18593  metustexhalf  18594  dyadmbllem  19491  atexch  23884  sstotbnd3  26485  pm14.123b  27603  ordpss  27630  climreeq  27715  reuan  27934  2reu1  27940  3cyclfrgrarn2  28404  eqlkr3  29899  dihatexv  32136  dvh3dim2  32246
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 178  df-an 361
  Copyright terms: Public domain W3C validator