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  8561  oaordex  8569  odi  8590  pssnn  9187  alephval3  10192  dfac2b  10212  axdc4lem  10536  leexp1a  14321  wrdsymb0  14697  coprmproddvds  16843  lmodvsmmulgdi  21177  assamulgscm  22214  2ndcctbss  23779  2pthnloop  30322  wwlksnext  30487  umgr2cycllem  30751  frgrregord013  31001  atcvatlem  32992  exp5g  37184  cdleme48gfv1  41686  cdlemg6e  41772  dihord5apre  42412  dihglblem5apreN  42441  iccpartgt  48602  lmodvsmdi  49584  nn0sumshdiglemB  49825