Theorem exp4c 434

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 417	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏)))
3	2	expd 417	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  exp5j  447  oawordri  8479  oaordex  8487  odi  8508  pssnn  9097  alephval3  10027  dfac2b  10048  axdc4lem  10373  leexp1a  14132  wrdsymb0  14506  coprmproddvds  16627  lmodvsmmulgdi  20890  assamulgscm  21879  2ndcctbss  23441  2pthnloop  29819  wwlksnext  29981  frgrregord013  30485  atcvatlem  32476  umgr2cycllem  35381  exp5g  36544  cdleme48gfv1  41041  cdlemg6e  41127  dihord5apre  41767  dihglblem5apreN  41796  iccpartgt  47914  lmodvsmdi  48882  nn0sumshdiglemB  49123