Theorem exp4c 438

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  exp5j  451  oawordri  8586  oaordex  8594  odi  8615  pssnn  9212  alephval3  10216  dfac2b  10236  axdc4lem  10560  leexp1a  14345  wrdsymb0  14721  coprmproddvds  16867  lmodvsmmulgdi  21202  assamulgscm  22239  2ndcctbss  23804  2pthnloop  30347  wwlksnext  30512  umgr2cycllem  30776  frgrregord013  31026  atcvatlem  33017  exp5g  37270  cdleme48gfv1  41785  cdlemg6e  41871  dihord5apre  42511  dihglblem5apreN  42540  iccpartgt  48714  lmodvsmdi  49696  nn0sumshdiglemB  49937