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 25 . 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 187  df-an 371
This theorem is referenced by:  impac  621  equviniv  1829  2eu1OLD  2330  reupick  3736  prel12  4151  reusv2lem3  4599  ssrnres  5265  funmo  5587  funssres  5611  dffo4  6027  dffo5  6028  dfwe2  6601  ordpwsuc  6635  ordunisuc2  6664  dfom2  6687  nnsuc  6702  nnaordex  7326  wdom2d  8042  iundom2g  8949  fzospliti  11891  hash2sspr  12577  rexuz3  13332  qredeq  14458  dirge  16193  lssssr  17921  lpigen  18226  psgnodpm  18924  neiptopnei  19928  metustexhalfOLD  21360  metustexhalf  21361  dyadmbllem  22302  3cyclfrgrarn2  25443  atexch  27726  ordtconlem1  28372  isbasisrelowllem1  31285  isbasisrelowllem2  31286  sstotbnd3  31567  eqlkr3  32132  dihatexv  34371  dvh3dim2  34481  pm14.123b  36194  ordpss  36221  climreeq  37000  reuan  37566  2reu1  37572
  Copyright terms: Public domain W3C validator