Theorem exp4c 419

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

Syntax hints:   → wi 4   ∧ wa 382

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 383

This theorem is referenced by:  exp5j  432  oawordri  7788  oaordex  7796  odi  7817  pssnn  8338  alephval3  9137  dfac2b  9157  dfac2OLD  9159  axdc4lem  9483  leexp1a  13126  wrdsymb0  13535  swrdnd2  13642  coprmproddvds  15584  lmodvsmmulgdi  19108  assamulgscm  19565  2ndcctbss  21479  2pthnloop  26862  wwlksnext  27037  frgrregord013  27594  atcvatlem  29584  exp5g  32634  cdleme48gfv1  36344  cdlemg6e  36430  dihord5apre  37070  dihglblem5apreN  37099  iccpartgt  41886  lmodvsmdi  42686  lindslinindsimp1  42769  nn0sumshdiglemB  42937