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  5618  tz7.7  6343  oalimcl  8487  unbenlem  16836  rnelfm  23897  conway  27775  uspgr2wlkeqi  29721  1pthon2v  30228  spansncvi  31727  atom1d  32428  chirredlem3  32467  finminlem  36512  regsfromregtr  36668  cvlcvr1  39599  lhpexle2lem  40269  trlord  40829  cdlemkid4  41194  dihord6apre  41516  dihglbcpreN  41560