exp42 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > exp42		Structured version Visualization version GIF version

Theorem exp42 435

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

**Hypothesis**
Ref	Expression
exp42.1	⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)

**Assertion**
Ref	Expression
exp42	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

**Proof of Theorem exp42**
Step	Hyp	Ref	Expression
1		exp42.1	. . 3 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)
2	1	exp31 419	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏)))
3	2	expd 415	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395

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

This theorem depends on definitions: df-bi 206 df-an 396

This theorem is referenced by: isofrlem 7348 f1ocnv2d 7674 oelim 8555 zorn2lem7 10526 addrid 11425 initoeu1 18000 termoeu1 18007 issubg4 19100 lmodvsdir 20769 lmodvsass 20770 gsummatr01lem4 22573 dvfsumrlim3 25981 wwlksext2clwwlk 29880 shscli 31140 f1o3d 32425 slmdvsdir 32936 slmdvsass 32937 lshpcmp 38460

	
		OSZAR »