Theorem exp4c 635

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  exp5j  644  oawordri  7675  oaordex  7683  odi  7704  pssnn  8219  alephval3  8971  dfac2  8991  axdc4lem  9315  leexp1a  12959  wrdsymb0  13371  swrdnd2  13479  coprmproddvds  15424  lmodvsmmulgdi  18946  assamulgscm  19398  2ndcctbss  21306  2pthnloop  26683  wwlksnext  26856  frgrregord013  27382  atcvatlem  29372  exp5g  32422  cdleme48gfv1  36141  cdlemg6e  36227  dihord5apre  36868  dihglblem5apreN  36897  iccpartgt  41688  lmodvsmdi  42488  lindslinindsimp1  42571  nn0sumshdiglemB  42739