Theorem exp42 440

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 424	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏)))
3	2	expd 420	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  isofrlem  7328  f1ocnv2d  7653  oelim  8507  zorn2lem7  10474  addrid  11378  initoeu1  18058  termoeu1  18065  issubg4  19203  lmodvsdir  20976  lmodvsass  20977  gsummatr01lem4  22776  dvfsumrlim3  26153  wwlksext2clwwlk  30317  shscli  31578  f1o3d  32883  slmdvsdir  33449  slmdvsass  33450  lshpcmp  39624  relpfrlem  45527