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  8478  oaordex  8486  odi  8507  pssnn  9096  alephval3  10023  dfac2b  10044  axdc4lem  10368  leexp1a  14128  wrdsymb0  14502  coprmproddvds  16623  lmodvsmmulgdi  20883  assamulgscm  21891  2ndcctbss  23430  2pthnloop  29814  wwlksnext  29976  frgrregord013  30480  atcvatlem  32471  umgr2cycllem  35338  exp5g  36501  cdleme48gfv1  40996  cdlemg6e  41082  dihord5apre  41722  dihglblem5apreN  41751  iccpartgt  47899  lmodvsmdi  48867  nn0sumshdiglemB  49108