ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.43d Structured version   GIF version

Theorem pm2.43d 44
Description: Deduction absorbing redundant antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.)
Hypothesis
Ref Expression
pm2.43d.1 (φ → (ψ → (ψχ)))
Assertion
Ref Expression
pm2.43d (φ → (ψχ))

Proof of Theorem pm2.43d
StepHypRef Expression
1 id 19 . 2 (ψψ)
2 pm2.43d.1 . 2 (φ → (ψ → (ψχ)))
31, 2mpdi 38 1 (φ → (ψχ))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  loolin  95  pm2.18dc  741  sbcof2  1673  rgen2a  2353  rspct  2626  po2nr  4020  ordsuc  4225  funssres  4868  2elresin  4936  f1imass  5338  smoel  5837  tfri3  5875  nnmass  5981  genpcdl  6374  genpcuu  6375  recexprlemss1l  6469  recexprlemss1u  6470  elabgft1  7024  bj-rspgt  7032
  Copyright terms: Public domain W3C validator