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  7333  f1ocnv2d  7660  oelim  8546  zorn2lem7  10516  addrid  11415  initoeu1  18024  termoeu1  18031  issubg4  19128  lmodvsdir  20843  lmodvsass  20844  gsummatr01lem4  22596  dvfsumrlim3  25992  wwlksext2clwwlk  30038  shscli  31298  f1o3d  32605  slmdvsdir  33213  slmdvsass  33214  lshpcmp  39006  relpfrlem  44978