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  860  sbcof2  1856  rgen2a  2584  rspct  2900  po2nr  4401  ordsuc  4656  funssres  5363  2elresin  5437  f1imass  5907  smoel  6457  tfri3  6524  nnmass  6646  sbthlem1  7140  genpcdl  7722  genpcuu  7723  recexprlemss1l  7838  recexprlemss1u  7839  grpid  13593  uniopn  14696  elabgft1  16251  bj-rspgt  16259