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

Theorem pm2.43d 50
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 43 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  loolin  101  pm2.18dc  825  sbcof2  1766  rgen2a  2463  rspct  2756  po2nr  4201  ordsuc  4448  funssres  5135  2elresin  5204  f1imass  5643  smoel  6165  tfri3  6232  nnmass  6351  sbthlem1  6813  genpcdl  7295  genpcuu  7296  recexprlemss1l  7411  recexprlemss1u  7412  uniopn  12095  elabgft1  12912  bj-rspgt  12920
  Copyright terms: Public domain W3C validator