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  102  pm2.18dc  856  sbcof2  1820  rgen2a  2541  rspct  2846  po2nr  4321  ordsuc  4574  funssres  5270  2elresin  5339  f1imass  5788  smoel  6315  tfri3  6382  nnmass  6502  sbthlem1  6970  genpcdl  7532  genpcuu  7533  recexprlemss1l  7648  recexprlemss1u  7649  grpid  12936  uniopn  13797  elabgft1  14826  bj-rspgt  14834
  Copyright terms: Public domain W3C validator