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  749  sbcof2  1688  rgen2a  2369  rspct  2643  po2nr  4037  ordsuc  4241  funssres  4885  2elresin  4953  f1imass  5356  smoel  5856  tfri3  5894  nnmass  6005  genpcdl  6502  genpcuu  6503  recexprlemss1l  6605  recexprlemss1u  6606  elabgft1  9186  bj-rspgt  9194
  Copyright terms: Public domain W3C validator