Theorem exp44 437

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 420	. 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:  wefrc  5632  tz7.7  6358  oalimcl  8524  unbenlem  16879  rnelfm  23840  conway  27711  uspgr2wlkeqi  29576  1pthon2v  30082  spansncvi  31581  atom1d  32282  chirredlem3  32321  finminlem  36306  cvlcvr1  39332  lhpexle2lem  40003  trlord  40563  cdlemkid4  40928  dihord6apre  41250  dihglbcpreN  41294