Theorem exp4c 436

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  exp5j  449  oawordri  8220  oaordex  8228  odi  8249  pssnn  8780  pssnnOLD  8828  alephval3  9623  dfac2b  9643  axdc4lem  9968  leexp1a  13644  wrdsymb0  14003  coprmproddvds  16117  lmodvsmmulgdi  19801  assamulgscm  20728  2ndcctbss  22219  2pthnloop  27685  wwlksnext  27844  frgrregord013  28345  atcvatlem  30333  umgr2cycllem  32686  exp5g  34148  cdleme48gfv1  38206  cdlemg6e  38292  dihord5apre  38932  dihglblem5apreN  38961  iccpartgt  44461  lmodvsmdi  45300  nn0sumshdiglemB  45548