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  8465  oaordex  8473  odi  8494  pssnn  9078  alephval3  9998  dfac2b  10019  axdc4lem  10343  leexp1a  14079  wrdsymb0  14453  coprmproddvds  16571  lmodvsmmulgdi  20828  assamulgscm  21836  2ndcctbss  23368  2pthnloop  29707  wwlksnext  29869  frgrregord013  30370  atcvatlem  32360  umgr2cycllem  35172  exp5g  36336  cdleme48gfv1  40574  cdlemg6e  40660  dihord5apre  41300  dihglblem5apreN  41329  iccpartgt  47457  lmodvsmdi  48409  nn0sumshdiglemB  48651