Theorem exp4c 634

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

This theorem is referenced by:  exp5j  643  oawordri  7517  oaordex  7525  odi  7546  pssnn  8063  alephval3  8816  dfac2  8836  axdc4lem  9160  leexp1a  12781  wrdsymb0  13194  swrdnd2  13285  coprmproddvds  15215  lmodvsmmulgdi  18721  assamulgscm  19171  2ndcctbss  21068  wwlknext  26252  frgraregord013  26645  atcvatlem  28628  exp5g  31467  cdleme48gfv1  34842  cdlemg6e  34928  dihord5apre  35569  dihglblem5apreN  35598  iccpartgt  39965  2pthnloop  40937  wwlksnext  41099  av-frgraregord013  41549  lmodvsmdi  41957  lindslinindsimp1  42040  nn0sumshdiglemB  42212