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  8541  oaordex  8549  odi  8570  pssnn  9167  alephval3  10117  dfac2b  10137  axdc4lem  10461  leexp1a  14243  wrdsymb0  14618  coprmproddvds  16759  lmodvsmmulgdi  21087  assamulgscm  22122  2ndcctbss  23687  2pthnloop  30204  wwlksnext  30369  umgr2cycllem  30633  frgrregord013  30883  atcvatlem  32874  exp5g  36931  cdleme48gfv1  41417  cdlemg6e  41503  dihord5apre  42143  dihglblem5apreN  42172  iccpartgt  48335  lmodvsmdi  49317  nn0sumshdiglemB  49558