Theorem exp4c 432

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 415	. 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:  exp5j  445  oawordri  8475  oaordex  8483  odi  8504  pssnn  9092  alephval3  10023  dfac2b  10044  axdc4lem  10368  leexp1a  14100  wrdsymb0  14474  coprmproddvds  16592  lmodvsmmulgdi  20818  assamulgscm  21826  2ndcctbss  23358  2pthnloop  29694  wwlksnext  29856  frgrregord013  30357  atcvatlem  32347  umgr2cycllem  35112  exp5g  36276  cdleme48gfv1  40515  cdlemg6e  40601  dihord5apre  41241  dihglblem5apreN  41270  iccpartgt  47412  lmodvsmdi  48364  nn0sumshdiglemB  48606