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  8514  oaordex  8522  odi  8543  pssnn  9132  alephval3  10063  dfac2b  10084  axdc4lem  10408  leexp1a  14140  wrdsymb0  14514  coprmproddvds  16633  lmodvsmmulgdi  20803  assamulgscm  21810  2ndcctbss  23342  2pthnloop  29661  wwlksnext  29823  frgrregord013  30324  atcvatlem  32314  umgr2cycllem  35127  exp5g  36291  cdleme48gfv1  40530  cdlemg6e  40616  dihord5apre  41256  dihglblem5apreN  41285  iccpartgt  47428  lmodvsmdi  48367  nn0sumshdiglemB  48609