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

Theorem ancrd 578
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 556 1 (𝜑 → (𝜓 → (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  impac  652  equviniva  2101  reupick  4042  prel12OLD  4515  reusv2lem3  5008  ssrelrn  5458  ssrnres  5718  funmo  6053  funssres  6079  dffo4  6526  dffo5  6527  dfwe2  7134  ordpwsuc  7168  ordunisuc2  7197  dfom2  7220  nnsuc  7235  nnaordex  7875  wdom2d  8638  iundom2g  9525  fzospliti  12665  rexuz3  14258  qredeq  15544  prmdvdsfz  15590  dirge  17409  lssssr  19126  lpigen  19429  psgnodpm  20107  neiptopnei  21109  metustexhalf  22533  dyadmbllem  23538  3cyclfrgrrn2  27412  atexch  29520  ordtconnlem1  30250  isbasisrelowllem1  33485  isbasisrelowllem2  33486  phpreu  33675  poimirlem26  33717  sstotbnd3  33857  eqlkr3  34860  dihatexv  37098  dvh3dim2  37208  neik0pk1imk0  38816  pm14.123b  39098  ordpss  39126  climreeq  40317  reuan  41655  2reu1  41661
  Copyright terms: Public domain W3C validator