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

Theorem ancrd 575
 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 196  df-an 385 This theorem is referenced by:  impac  649  equviniva  1947  reupick  3870  prel12  4323  reusv2lem3  4797  ssrelrn  5237  ssrnres  5491  funmo  5820  funssres  5844  dffo4  6283  dffo5  6284  dfwe2  6873  ordpwsuc  6907  ordunisuc2  6936  dfom2  6959  nnsuc  6974  nnaordex  7605  wdom2d  8368  iundom2g  9241  fzospliti  12369  rexuz3  13936  qredeq  15209  prmdvdsfz  15255  dirge  17060  lssssr  18774  lpigen  19077  psgnodpm  19753  neiptopnei  20746  metustexhalf  22171  dyadmbllem  23173  3cyclfrgrarn2  26541  atexch  28624  ordtconlem1  29298  isbasisrelowllem1  32379  isbasisrelowllem2  32380  phpreu  32563  poimirlem26  32605  sstotbnd3  32745  eqlkr3  33406  dihatexv  35645  dvh3dim2  35755  neik0pk1imk0  37365  pm14.123b  37649  ordpss  37676  climreeq  38680  reuan  39829  2reu1  39835  3cyclfrgrrn2  41457
 Copyright terms: Public domain W3C validator