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  8542  oaordex  8550  odi  8571  pssnn  9168  alephval3  10170  dfac2b  10190  axdc4lem  10514  leexp1a  14298  wrdsymb0  14674  coprmproddvds  16818  lmodvsmmulgdi  21152  assamulgscm  22189  2ndcctbss  23754  2pthnloop  30299  wwlksnext  30464  umgr2cycllem  30728  frgrregord013  30978  atcvatlem  32969  exp5g  37062  cdleme48gfv1  41561  cdlemg6e  41647  dihord5apre  42287  dihglblem5apreN  42316  iccpartgt  48453  lmodvsmdi  49435  nn0sumshdiglemB  49676