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  8471  oaordex  8479  odi  8500  pssnn  9085  alephval3  10008  dfac2b  10029  axdc4lem  10353  leexp1a  14084  wrdsymb0  14458  coprmproddvds  16576  lmodvsmmulgdi  20832  assamulgscm  21840  2ndcctbss  23371  2pthnloop  29711  wwlksnext  29873  frgrregord013  30377  atcvatlem  32367  umgr2cycllem  35205  exp5g  36368  cdleme48gfv1  40655  cdlemg6e  40741  dihord5apre  41381  dihglblem5apreN  41410  iccpartgt  47551  lmodvsmdi  48503  nn0sumshdiglemB  48745