Theorem exp42 441

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  isofrlem  7348  f1ocnv2d  7674  oelim  8545  zorn2lem7  10583  addrid  11493  initoeu1  18191  termoeu1  18198  issubg4  19361  lmodvsdir  21166  lmodvsass  21167  gsummatr01lem4  22978  dvfsumrlim3  26358  wwlksext2clwwlk  30653  shscli  31924  f1o3d  33267  slmdvsdir  33823  slmdvsass  33824  lshpcmp  40138  relpfrlem  46036