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  8516  oaordex  8524  odi  8545  pssnn  9137  alephval3  10069  dfac2b  10090  axdc4lem  10414  leexp1a  14146  wrdsymb0  14520  coprmproddvds  16639  lmodvsmmulgdi  20809  assamulgscm  21816  2ndcctbss  23348  2pthnloop  29667  wwlksnext  29829  frgrregord013  30330  atcvatlem  32320  umgr2cycllem  35127  exp5g  36286  cdleme48gfv1  40525  cdlemg6e  40611  dihord5apre  41251  dihglblem5apreN  41280  iccpartgt  47418  lmodvsmdi  48357  nn0sumshdiglemB  48599