Theorem exp4c 437

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  exp5j  450  oawordri  8523  oaordex  8531  odi  8552  pssnn  9141  alephval3  10082  dfac2b  10102  axdc4lem  10427  leexp1a  14202  wrdsymb0  14576  coprmproddvds  16711  lmodvsmmulgdi  20987  assamulgscm  22011  2ndcctbss  23573  2pthnloop  29989  wwlksnext  30151  frgrregord013  30655  atcvatlem  32646  umgr2cycllem  35503  exp5g  36676  cdleme48gfv1  41172  cdlemg6e  41258  dihord5apre  41898  dihglblem5apreN  41927  iccpartgt  48031  lmodvsmdi  49010  nn0sumshdiglemB  49251