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  1803  2eu1OLD  2377  reupick  3781  prel12  4207  reusv2lem3  4655  ssrnres  5450  funmo  5609  funssres  5633  dffo4  6047  dffo5  6048  dfwe2  6617  ordpwsuc  6650  ordunisuc2  6679  dfom2  6702  nnsuc  6717  nnaordex  7306  wdom2d  8027  iundom2g  8936  fzospliti  11857  hash2sspr  12526  rexuz3  13181  qredeq  14247  dirge  15867  lssssr  17599  lpigen  17904  psgnodpm  18624  neiptopnei  19633  metustexhalfOLD  21066  metustexhalf  21067  dyadmbllem  22008  3cyclfrgrarn2  25014  atexch  27300  ordtconlem1  27906  sstotbnd3  30272  pm14.123b  31333  ordpss  31360  climreeq  31619  reuan  32185  2reu1  32191  eqlkr3  34826  dihatexv  37065  dvh3dim2  37175
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