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  102  pm2.18dc  856  sbcof2  1821  rgen2a  2544  rspct  2849  po2nr  4327  ordsuc  4580  funssres  5277  2elresin  5346  f1imass  5796  smoel  6325  tfri3  6392  nnmass  6512  sbthlem1  6986  genpcdl  7548  genpcuu  7549  recexprlemss1l  7664  recexprlemss1u  7665  grpid  12983  uniopn  13958  elabgft1  14988  bj-rspgt  14996