Theorem exp4c 432

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  exp5j  445  oawordri  8562  oaordex  8570  odi  8591  pssnn  9182  alephval3  10124  dfac2b  10145  axdc4lem  10469  leexp1a  14193  wrdsymb0  14567  coprmproddvds  16682  lmodvsmmulgdi  20854  assamulgscm  21861  2ndcctbss  23393  2pthnloop  29713  wwlksnext  29875  frgrregord013  30376  atcvatlem  32366  umgr2cycllem  35162  exp5g  36321  cdleme48gfv1  40555  cdlemg6e  40641  dihord5apre  41281  dihglblem5apreN  41310  iccpartgt  47441  lmodvsmdi  48354  nn0sumshdiglemB  48600