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

Theorem ancrd 553
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 514 1 (𝜑 → (𝜓 → (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  impac  554  equvinva  2034  sbcg  3822  reuan  3856  2reu1  3857  reupick  4282  reusv2lem3  5359  ssrelrn  5854  relssres  5982  funmo  6520  funmoOLD  6521  funssres  6549  dffo4  7057  dffo5  7058  dfwe2  7712  ordpwsuc  7754  ordunisuc2  7784  dfom2  7808  nnsuc  7824  nnaordex  8589  wdom2d  9524  iundom2g  10484  fzospliti  13613  rexuz3  15242  qredeq  16541  prmdvdsfz  16589  dirge  18500  lssssr  20458  lpigen  20771  psgnodpm  21015  neiptopnei  22506  metustexhalf  23935  dyadmbllem  24986  3cyclfrgrrn2  29280  atexch  31372  ordtconnlem1  32569  bj-ideqg1  35685  bj-imdirval3  35705  isbasisrelowllem1  35876  isbasisrelowllem2  35877  pibt2  35938  phpreu  36112  poimirlem26  36154  sstotbnd3  36285  eqlkr3  37613  dihatexv  39851  dvh3dim2  39961  prjspner1  41011  oasubex  41668  naddwordnexlem4  41765  neik0pk1imk0  42411  pm14.123b  42798  ordpss  42823  climreeq  43944  itscnhlc0xyqsol  46941
  Copyright terms: Public domain W3C validator