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 554 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  650  equviniva  2004  reupick  3944  prel12  4414  reusv2lem3  4901  ssrelrn  5347  ssrnres  5607  funmo  5942  funssres  5968  dffo4  6415  dffo5  6416  dfwe2  7023  ordpwsuc  7057  ordunisuc2  7086  dfom2  7109  nnsuc  7124  nnaordex  7763  wdom2d  8526  iundom2g  9400  fzospliti  12539  rexuz3  14132  qredeq  15418  prmdvdsfz  15464  dirge  17284  lssssr  19001  lpigen  19304  psgnodpm  19982  neiptopnei  20984  metustexhalf  22408  dyadmbllem  23413  3cyclfrgrrn2  27267  atexch  29368  ordtconnlem1  30098  isbasisrelowllem1  33333  isbasisrelowllem2  33334  phpreu  33523  poimirlem26  33565  sstotbnd3  33705  eqlkr3  34706  dihatexv  36944  dvh3dim2  37054  neik0pk1imk0  38662  pm14.123b  38944  ordpss  38972  climreeq  40163  reuan  41501  2reu1  41507
  Copyright terms: Public domain W3C validator