pm2.43i - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > pm2.43i		GIF version

Theorem pm2.43i 43

Description: Inference absorbing redundant antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.)

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

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

**Proof of Theorem pm2.43i**
Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (φ → φ)
2		pm2.43i.1	. 2 ⊢ (φ → (φ → ψ))
3	1, 2	mpd 14	1 ⊢ (φ → ψ)

Colors of variables: wff setvar class

Syntax hints: → wi 4

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 8

This theorem is referenced by: sylc 56 pm2.18 102 impbid 183 ibi 232 anidms 626 tbw-bijust 1463 tbw-negdf 1464 equid 1676 equidOLD 1677 hbae 1953 aecom-o 2151 hbae-o 2153 hbequid 2160 equidqe 2173 equid1ALT 2176 ax10from10o 2177 ax11inda 2200 vtoclgaf 2919 vtocl2gaf 2921 vtocl3gaf 2923 elinti 3935 spfinsfincl 4539 copsexg 4607