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  8517  oaordex  8525  odi  8546  pssnn  9138  alephval3  10070  dfac2b  10091  axdc4lem  10415  leexp1a  14147  wrdsymb0  14521  coprmproddvds  16640  lmodvsmmulgdi  20810  assamulgscm  21817  2ndcctbss  23349  2pthnloop  29668  wwlksnext  29830  frgrregord013  30331  atcvatlem  32321  umgr2cycllem  35134  exp5g  36298  cdleme48gfv1  40537  cdlemg6e  40623  dihord5apre  41263  dihglblem5apreN  41292  iccpartgt  47432  lmodvsmdi  48371  nn0sumshdiglemB  48613