Theorem pm2.43d 53

Description: Deduction absorbing redundant antecedent. Deduction associated with pm2.43 56 and pm2.43i 52. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Mel L. 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 22	. 2 ⊢ (𝜓 → 𝜓)
2		pm2.43d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒)))
3	1, 2	mpdi 45	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  111  rspct  3547  po2nr  5517  somo  5540  ordelord  6288  tz7.7  6292  funssres  6478  2elresin  6553  dffv2  6863  f1imass  7137  onint  7640  wfrlem12OLD  8151  wfrlem14OLD  8153  onfununi  8172  smoel  8191  tfrlem11  8219  tfr3  8230  omass  8411  nnmass  8455  sbthlem1  8870  pssnn  8951  php  8993  phpOLD  9005  inf3lem2  9387  cardne  9723  dfac2b  9886  indpi  10663  genpcd  10762  ltexprlem7  10798  addcanpr  10802  reclem4pr  10806  suplem2pr  10809  sup2  11931  nnunb  12229  uzwo  12651  xrub  13046  grpid  18615  lsmcss  20897  uniopn  22046  fclsss1  23173  fclsss2  23174  grpoid  28882  spansncvi  30014  pjnormssi  30530  sumdmdlem2  30781  acycgrcycl  33109  sltval2  33859  meran1  34600  bj-animbi  34739  currysetlem2  35137  bj-elsn0  35326  poimirlem31  35808  heicant  35812  hlhilhillem  39978  sn-sup2  40439  ee223  42254  eel2122old  42338  afv0nbfvbi  44643  fmtnoprmfac1lem  45016