MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancrd 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
Assertion
Ref Expression
ancrd

Proof of Theorem ancrd
StepHypRef Expression
1 ancrd.1 . 2
2 idd 24 . 2
31, 2jcad 533 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  impac  621  equviniv  1743  euanOLD  2341  2eu1OLD  2374  reupick  3748  prel12  4166  reusv2lem3  4612  ssrnres  5395  funmo  5553  funssres  5577  dffo4  5982  dffo5  5983  dfwe2  6526  ordpwsuc  6559  ordunisuc2  6588  dfom2  6611  nnsuc  6626  nnaordex  7211  wdom2d  7932  iundom2g  8841  fzospliti  11726  rexuz3  12994  qredeq  13950  dirge  15566  lssssr  17210  lpigen  17514  psgnodpm  18211  neiptopnei  19135  metustexhalfOLD  20537  metustexhalf  20538  dyadmbllem  21479  atexch  26254  ordtconlem1  26811  sstotbnd3  29135  pm14.123b  30140  ordpss  30167  climreeq  30384  reuan  30881  2reu1  30887  hash2sspr  31104  3cyclfrgrarn2  31483  eqlkr3  33597  dihatexv  35834  dvh3dim2  35944
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
  Copyright terms: Public domain W3C validator