Theorem exp4c 435

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  exp5j  448  oawordri  8170  oaordex  8178  odi  8199  pssnn  8730  alephval3  9530  dfac2b  9550  axdc4lem  9871  leexp1a  13533  wrdsymb0  13895  coprmproddvds  16001  lmodvsmmulgdi  19663  assamulgscm  20124  2ndcctbss  22057  2pthnloop  27506  wwlksnext  27665  frgrregord013  28168  atcvatlem  30156  umgr2cycllem  32382  exp5g  33646  cdleme48gfv1  37666  cdlemg6e  37752  dihord5apre  38392  dihglblem5apreN  38421  iccpartgt  43581  lmodvsmdi  44424  nn0sumshdiglemB  44674