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  8477  oaordex  8485  odi  8506  pssnn  9093  alephval3  10020  dfac2b  10041  axdc4lem  10365  leexp1a  14098  wrdsymb0  14472  coprmproddvds  16590  lmodvsmmulgdi  20848  assamulgscm  21857  2ndcctbss  23399  2pthnloop  29804  wwlksnext  29966  frgrregord013  30470  atcvatlem  32460  umgr2cycllem  35334  exp5g  36497  cdleme48gfv1  40792  cdlemg6e  40878  dihord5apre  41518  dihglblem5apreN  41547  iccpartgt  47669  lmodvsmdi  48621  nn0sumshdiglemB  48862