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  1824  rgen2a  2551  rspct  2861  po2nr  4345  ordsuc  4600  funssres  5301  2elresin  5372  f1imass  5824  smoel  6367  tfri3  6434  nnmass  6554  sbthlem1  7032  genpcdl  7605  genpcuu  7606  recexprlemss1l  7721  recexprlemss1u  7722  grpid  13243  uniopn  14323  elabgft1  15510  bj-rspgt  15518