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

Theorem ancrd 552
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 513 1 (𝜑 → (𝜓 → (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  impac  553  equvinva  2028  reuan  3877  2reu1  3878  reupick  4284  reusv2lem3  5291  ssrelrn  5756  relssres  5886  funmo  6364  funssres  6391  dffo4  6861  dffo5  6862  dfwe2  7485  ordpwsuc  7519  ordunisuc2  7548  dfom2  7571  nnsuc  7586  nnaordex  8253  wdom2d  9032  iundom2g  9950  fzospliti  13057  rexuz3  14696  qredeq  15989  prmdvdsfz  16037  dirge  17835  lssssr  19654  lpigen  19957  psgnodpm  20660  neiptopnei  21668  metustexhalf  23093  dyadmbllem  24127  3cyclfrgrrn2  27993  atexch  30085  ordtconnlem1  31066  bj-ideqg1  34348  bj-imdirval3  34366  bj-imdirid  34367  isbasisrelowllem1  34518  isbasisrelowllem2  34519  pibt2  34580  phpreu  34757  poimirlem26  34799  sstotbnd3  34935  eqlkr3  36117  dihatexv  38354  dvh3dim2  38464  neik0pk1imk0  40275  pm14.123b  40635  ordpss  40660  climreeq  41770  itscnhlc0xyqsol  44680
  Copyright terms: Public domain W3C validator