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  8487  oaordex  8495  odi  8516  pssnn  9105  alephval3  10032  dfac2b  10053  axdc4lem  10377  leexp1a  14110  wrdsymb0  14484  coprmproddvds  16602  lmodvsmmulgdi  20860  assamulgscm  21869  2ndcctbss  23411  2pthnloop  29816  wwlksnext  29978  frgrregord013  30482  atcvatlem  32472  umgr2cycllem  35353  exp5g  36516  cdleme48gfv1  40906  cdlemg6e  40992  dihord5apre  41632  dihglblem5apreN  41661  iccpartgt  47781  lmodvsmdi  48733  nn0sumshdiglemB  48974