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  863  sbcof2  1859  rgen2a  2598  rspct  2916  po2nr  4432  ordsuc  4687  funssres  5397  2elresin  5471  f1imass  5949  smoel  6533  tfri3  6600  nnmass  6722  sbthlem1  7229  genpcdl  7839  genpcuu  7840  recexprlemss1l  7955  recexprlemss1u  7956  grpid  13773  uniopn  14915  elabgft1  16599  bj-rspgt  16607