Theorem exp4c 423

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  exp5j  436  oawordri  7837  oaordex  7845  odi  7866  pssnn  8387  alephval3  9186  dfac2b  9206  dfac2OLD  9208  axdc4lem  9532  leexp1a  13129  wrdsymb0  13523  swrdnd2  13638  coprmproddvds  15660  lmodvsmmulgdi  19170  assamulgscm  19627  2ndcctbss  21541  2pthnloop  26922  wwlksnext  27099  frgrregord013  27714  atcvatlem  29703  exp5g  32744  cdleme48gfv1  36495  cdlemg6e  36581  dihord5apre  37221  dihglblem5apreN  37250  iccpartgt  42100  lmodvsmdi  42835  lindslinindsimp1  42918  nn0sumshdiglemB  43086