Theorem exp44 443

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

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

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 402

This theorem is used by:  wefrc  5645  tz7.7  6381  oalimcl  8552  unbenlem  17066  rnelfm  24252  conway  28147  uspgr2wlkeqi  30210  1pthon2v  30736  spansncvi  32236  atom1d  32937  chirredlem3  32976  finminlem  37076  regsfromregtco  37296  cvlcvr1  40364  lhpexle2lem  41034  trlord  41594  cdlemkid4  41959  dihord6apre  42281  dihglbcpreN  42325