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

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜓 → 𝜓)
2		pm2.43d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒)))
3	1, 2	mpdi 43	1 ⊢ (𝜑 → (𝜓 → 𝜒))

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  841  sbcof2  1783  rgen2a  2489  rspct  2786  po2nr  4239  ordsuc  4486  funssres  5173  2elresin  5242  f1imass  5683  smoel  6205  tfri3  6272  nnmass  6391  sbthlem1  6853  genpcdl  7351  genpcuu  7352  recexprlemss1l  7467  recexprlemss1u  7468  uniopn  12207  elabgft1  13156  bj-rspgt  13164