Theorem exp4c 433

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  exp5j  446  oawordri  8482  oaordex  8490  odi  8511  pssnn  9100  alephval3  10030  dfac2b  10051  axdc4lem  10375  leexp1a  14135  wrdsymb0  14509  coprmproddvds  16630  lmodvsmmulgdi  20894  assamulgscm  21883  2ndcctbss  23445  2pthnloop  29824  wwlksnext  29986  frgrregord013  30490  atcvatlem  32481  umgr2cycllem  35375  exp5g  36538  cdleme48gfv1  41035  cdlemg6e  41121  dihord5apre  41761  dihglblem5apreN  41790  iccpartgt  47909  lmodvsmdi  48877  nn0sumshdiglemB  49118