Theorem exp44 442

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  wefrc  5654  tz7.7  6386  oalimcl  8543  unbenlem  16974  rnelfm  24121  conway  27983  uspgr2wlkeqi  30008  1pthon2v  30515  spansncvi  32015  atom1d  32716  chirredlem3  32755  finminlem  36857  regsfromregtco  37077  cvlcvr1  40141  lhpexle2lem  40811  trlord  41371  cdlemkid4  41736  dihord6apre  42058  dihglbcpreN  42102