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

Theorem ancrd 542
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 503 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 198  df-an 384
This theorem is referenced by:  impac  543  equvinva  2120  reupick  4069  prel12OLD  4525  reusv2lem3  5014  ssrelrn  5465  ssrnres  5724  funmo  6058  funssres  6084  dffo4  6535  dffo5  6536  dfwe2  7149  ordpwsuc  7183  ordunisuc2  7212  dfom2  7235  nnsuc  7250  nnaordex  7893  wdom2d  8662  iundom2g  9585  fzospliti  12730  rexuz3  14318  qredeq  15599  prmdvdsfz  15644  dirge  17465  lssssr  19185  lssssrOLD  19186  lpigen  19491  psgnodpm  20169  neiptopnei  21177  metustexhalf  22601  dyadmbllem  23607  3cyclfrgrrn2  27490  atexch  29597  ordtconnlem1  30327  isbasisrelowllem1  33557  isbasisrelowllem2  33558  phpreu  33743  poimirlem26  33785  sstotbnd3  33923  eqlkr3  34925  dihatexv  37163  dvh3dim2  37273  neik0pk1imk0  38885  pm14.123b  39166  ordpss  39193  climreeq  40369  reuan  41725  2reu1  41731
  Copyright terms: Public domain W3C validator