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

Theorem ancrd 555
 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 516 1 (𝜑 → (𝜓 → (𝜒𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  impac  556  equvinva  2037  reuan  3825  2reu1  3826  reupick  4239  reusv2lem3  5266  ssrelrn  5727  relssres  5859  funmo  6340  funssres  6368  dffo4  6846  dffo5  6847  dfwe2  7478  ordpwsuc  7512  ordunisuc2  7541  dfom2  7564  nnsuc  7579  nnaordex  8249  wdom2d  9030  iundom2g  9953  fzospliti  13066  rexuz3  14702  qredeq  15993  prmdvdsfz  16041  dirge  17841  lssssr  19721  lpigen  20025  psgnodpm  20281  neiptopnei  21744  metustexhalf  23170  dyadmbllem  24210  3cyclfrgrrn2  28079  atexch  30171  ordtconnlem1  31289  bj-ideqg1  34595  bj-imdirval3  34615  isbasisrelowllem1  34788  isbasisrelowllem2  34789  pibt2  34850  phpreu  35057  poimirlem26  35099  sstotbnd3  35230  eqlkr3  36413  dihatexv  38650  dvh3dim2  38760  neik0pk1imk0  40765  pm14.123b  41145  ordpss  41170  climreeq  42270  itscnhlc0xyqsol  45193
 Copyright terms: Public domain W3C validator