Theorem exp4c 438

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

Hypothesis

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

Assertion

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

Proof of Theorem exp4c

Step	Hyp	Ref	Expression
1		exp4c.1	. . 3 ⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏))
2	1	expd 421	. 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:  exp5j  451  oawordri  8544  oaordex  8552  odi  8573  pssnn  9163  alephval3  10113  dfac2b  10133  axdc4lem  10457  leexp1a  14231  wrdsymb0  14606  coprmproddvds  16746  lmodvsmmulgdi  21055  assamulgscm  22088  2ndcctbss  23649  2pthnloop  30117  wwlksnext  30279  frgrregord013  30783  atcvatlem  32774  umgr2cycllem  35653  exp5g  36856  cdleme48gfv1  41351  cdlemg6e  41437  dihord5apre  42077  dihglblem5apreN  42106  iccpartgt  48217  lmodvsmdi  49200  nn0sumshdiglemB  49441