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 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

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 207  df-an 396

This theorem is referenced by:  isofrlem  7286  f1ocnv2d  7611  oelim  8461  zorn2lem7  10412  addrid  11313  initoeu1  17935  termoeu1  17942  issubg4  19075  lmodvsdir  20837  lmodvsass  20838  gsummatr01lem4  22602  dvfsumrlim3  25996  wwlksext2clwwlk  30132  shscli  31392  f1o3d  32704  slmdvsdir  33298  slmdvsass  33299  lshpcmp  39244  relpfrlem  45190