Theorem exp42 439

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  isofrlem  7320  f1ocnv2d  7645  oelim  8498  zorn2lem7  10456  addrid  11360  initoeu1  18027  termoeu1  18034  issubg4  19170  lmodvsdir  20933  lmodvsass  20934  gsummatr01lem4  22698  dvfsumrlim3  26075  wwlksext2clwwlk  30205  shscli  31466  f1o3d  32778  slmdvsdir  33357  slmdvsass  33358  lshpcmp  39576  relpfrlem  45493