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  4400  ordsuc  4655  funssres  5360  2elresin  5434  f1imass  5904  smoel  6452  tfri3  6519  nnmass  6641  sbthlem1  7132  genpcdl  7714  genpcuu  7715  recexprlemss1l  7830  recexprlemss1u  7831  grpid  13580  uniopn  14683  elabgft1  16166  bj-rspgt  16174