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  8485  oaordex  8493  odi  8514  pssnn  9103  alephval3  10032  dfac2b  10053  axdc4lem  10377  leexp1a  14137  wrdsymb0  14511  coprmproddvds  16632  lmodvsmmulgdi  20892  assamulgscm  21881  2ndcctbss  23420  2pthnloop  29799  wwlksnext  29961  frgrregord013  30465  atcvatlem  32456  umgr2cycllem  35322  exp5g  36485  cdleme48gfv1  40982  cdlemg6e  41068  dihord5apre  41708  dihglblem5apreN  41737  iccpartgt  47887  lmodvsmdi  48855  nn0sumshdiglemB  49096