Theorem exp4c 436

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  exp5j  449  oawordri  8514  oaordex  8522  odi  8543  pssnn  9133  alephval3  10063  dfac2b  10084  axdc4lem  10409  leexp1a  14185  wrdsymb0  14559  coprmproddvds  16680  lmodvsmmulgdi  20944  assamulgscm  21933  2ndcctbss  23495  2pthnloop  29877  wwlksnext  30039  frgrregord013  30543  atcvatlem  32534  umgr2cycllem  35454  exp5g  36627  cdleme48gfv1  41124  cdlemg6e  41210  dihord5apre  41850  dihglblem5apreN  41879  iccpartgt  47997  lmodvsmdi  48965  nn0sumshdiglemB  49206