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  7280  f1ocnv2d  7605  oelim  8455  zorn2lem7  10400  addrid  11300  initoeu1  17920  termoeu1  17927  issubg4  19060  lmodvsdir  20821  lmodvsass  20822  gsummatr01lem4  22574  dvfsumrlim3  25968  wwlksext2clwwlk  30039  shscli  31299  f1o3d  32610  slmdvsdir  33192  slmdvsass  33193  lshpcmp  39107  relpfrlem  45070