Theorem pm2.43i 58

Description: Inference absorbing redundant antecedent.

Hypothesis

Ref	Expression
pm2.43i.1	⊢ (φ → (φ → ψ))

Assertion

Ref	Expression
pm2.43i	⊢ (φ → ψ)

Proof of Theorem pm2.43i

Step	Hyp	Ref	Expression
1		pm2.43i.1	. 2 ⊢ (φ → (φ → ψ))
2		pm2.43 57	. 2 ⊢ ((φ → (φ → ψ)) → (φ → ψ))
3	1, 2	ax-mp 6	1 ⊢ (φ → ψ)

Syntax hints:   → wi 2

This theorem is referenced by:  pm2.43a 60  pm2.18 75  anidm 331  anidms 332  anabsi5 377  ibi 449  eqid 810  eq4 821  eq5 824  vtoclga 1387  elab3g 1420  copsexg 1902  ssiun2s 2020  tz7.7 2224  nsuceq0 2306  tfrlem2 2950  tfrlem9 2957  tfrlem11 2959  oprabval 3047  oprabvalig 3048  omcl 3139  oecl 3140  nnacl 3172  nnmcl 3173  nndi 3180  endom 3289  sbth 3359  zornlem6 3608  zornlem7 3609  mulcanpi 3821  indpi 3828  prcdpq 3891  ltaddpr 3934  reclem2pr 3951  reclem3pr 3952  nn1suc 4435  sqrle 4765  alephexp2 4956  pjin 5584  strlem1 5691

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org