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

Theorem ancrd 576
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 555 1 (𝜑 → (𝜓 → (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  impac  650  equviniva  1957  reupick  3887  prel12  4351  reusv2lem3  4831  ssrelrn  5275  ssrnres  5531  funmo  5863  funssres  5888  dffo4  6331  dffo5  6332  dfwe2  6928  ordpwsuc  6962  ordunisuc2  6991  dfom2  7014  nnsuc  7029  nnaordex  7663  wdom2d  8429  iundom2g  9306  fzospliti  12441  rexuz3  14022  qredeq  15295  prmdvdsfz  15341  dirge  17158  lssssr  18872  lpigen  19175  psgnodpm  19853  neiptopnei  20846  metustexhalf  22271  dyadmbllem  23273  3cyclfrgrrn2  27015  atexch  29086  ordtconnlem1  29749  isbasisrelowllem1  32832  isbasisrelowllem2  32833  phpreu  33022  poimirlem26  33064  sstotbnd3  33204  eqlkr3  33865  dihatexv  36104  dvh3dim2  36214  neik0pk1imk0  37824  pm14.123b  38106  ordpss  38134  climreeq  39246  reuan  40481  2reu1  40487
  Copyright terms: Public domain W3C validator