imim1d - New Foundations Explorer

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

Theorem imim1d 69

Description: Deduction adding nested consequents. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2012.)

**Hypothesis**
Ref	Expression
imim1d.1	⊢ (φ → (ψ → χ))

**Assertion**
Ref	Expression
imim1d	⊢ (φ → ((χ → θ) → (ψ → θ)))

**Proof of Theorem imim1d**
Step	Hyp	Ref	Expression
1		imim1d.1	. 2 ⊢ (φ → (ψ → χ))
2		idd 21	. 2 ⊢ (φ → (θ → θ))
3	1, 2	imim12d 68	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: imim1 70 expt 148 imbi1d 308 meredith 1404 19.23tOLD 1819 ax12olem3 1929 morimv 2252 2mo 2282 sstr2 3279 ssralv 3330 preaddccan2 4455 spacind 6287 nchoicelem12 6300