Theorem exp4c 437

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  exp5j  450  oawordri  8536  oaordex  8544  odi  8565  pssnn  9154  alephval3  10095  dfac2b  10115  axdc4lem  10440  leexp1a  14213  wrdsymb0  14588  coprmproddvds  16722  lmodvsmmulgdi  20999  assamulgscm  22032  2ndcctbss  23593  2pthnloop  30058  wwlksnext  30220  frgrregord013  30724  atcvatlem  32715  umgr2cycllem  35610  exp5g  36793  cdleme48gfv1  41288  cdlemg6e  41374  dihord5apre  42014  dihglblem5apreN  42043  iccpartgt  48153  lmodvsmdi  49136  nn0sumshdiglemB  49377