Theorem exp44 438

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
exp44.1	⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜏)

Assertion

Ref	Expression
exp44	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Proof of Theorem exp44

Step	Hyp	Ref	Expression
1		exp44.1	. . 3 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜏)
2	1	exp32 421	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏)))
3	2	expd 416	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  wefrc  5619  tz7.7  6343  oalimcl  8492  unbenlem  16877  rnelfm  23943  conway  27796  uspgr2wlkeqi  29741  1pthon2v  30248  spansncvi  31748  atom1d  32449  chirredlem3  32488  finminlem  36553  regsfromregtco  36773  cvlcvr1  39838  lhpexle2lem  40508  trlord  41068  cdlemkid4  41433  dihord6apre  41755  dihglbcpreN  41799