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

Theorem pm2.43d 48
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 42 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  99  pm2.18dc  761  sbcof2  1707  rgen2a  2392  rspct  2666  po2nr  4073  ordsuc  4314  funssres  4969  2elresin  5037  f1imass  5440  smoel  5945  tfri3  5983  nnmass  6096  genpcdl  6674  genpcuu  6675  recexprlemss1l  6790  recexprlemss1u  6791  elabgft1  10283  bj-rspgt  10291
  Copyright terms: Public domain W3C validator