Theorem exp4c 636

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  exp5j  645  oawordri  7630  oaordex  7638  odi  7659  pssnn  8178  alephval3  8933  dfac2  8953  axdc4lem  9277  leexp1a  12919  wrdsymb0  13339  swrdnd2  13433  coprmproddvds  15377  lmodvsmmulgdi  18898  assamulgscm  19350  2ndcctbss  21258  2pthnloop  26627  wwlksnext  26788  frgrregord013  27253  atcvatlem  29244  exp5g  32297  cdleme48gfv1  35824  cdlemg6e  35910  dihord5apre  36551  dihglblem5apreN  36580  iccpartgt  41363  lmodvsmdi  42163  lindslinindsimp1  42246  nn0sumshdiglemB  42414