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  8606  oaordex  8614  odi  8635  pssnn  9234  alephval3  10179  dfac2b  10200  axdc4lem  10524  leexp1a  14225  wrdsymb0  14597  coprmproddvds  16710  lmodvsmmulgdi  20917  assamulgscm  21944  2ndcctbss  23484  2pthnloop  29767  wwlksnext  29926  frgrregord013  30427  atcvatlem  32417  umgr2cycllem  35108  exp5g  36269  cdleme48gfv1  40493  cdlemg6e  40579  dihord5apre  41219  dihglblem5apreN  41248  iccpartgt  47301  lmodvsmdi  48107  nn0sumshdiglemB  48354