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

This theorem is referenced by:  exp5j  446  oawordri  8502  oaordex  8510  odi  8531  pssnn  9119  pssnnOLD  9216  alephval3  10055  dfac2b  10075  axdc4lem  10400  leexp1a  14090  wrdsymb0  14449  coprmproddvds  16550  lmodvsmmulgdi  20414  assamulgscm  21341  2ndcctbss  22843  2pthnloop  28742  wwlksnext  28901  frgrregord013  29402  atcvatlem  31390  umgr2cycllem  33821  exp5g  34851  cdleme48gfv1  39072  cdlemg6e  39158  dihord5apre  39798  dihglblem5apreN  39827  iccpartgt  45739  lmodvsmdi  46578  nn0sumshdiglemB  46826