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

This theorem is referenced by:  exp5j  445  oawordri  8343  oaordex  8351  odi  8372  pssnn  8913  pssnnOLD  8969  alephval3  9797  dfac2b  9817  axdc4lem  10142  leexp1a  13821  wrdsymb0  14180  coprmproddvds  16296  lmodvsmmulgdi  20073  assamulgscm  21015  2ndcctbss  22514  2pthnloop  28000  wwlksnext  28159  frgrregord013  28660  atcvatlem  30648  umgr2cycllem  33002  exp5g  34419  cdleme48gfv1  38477  cdlemg6e  38563  dihord5apre  39203  dihglblem5apreN  39232  iccpartgt  44767  lmodvsmdi  45606  nn0sumshdiglemB  45854