Theorem exp31 346

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
exp31.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
exp31	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem exp31

Step	Hyp	Ref	Expression
1		exp31.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
2	1	ex 108	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	ex 108	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101

This theorem is referenced by:  exp41  352  exp42  353  expl  360  exbiri  364  anasss  379  an31s  504  con4biddc  754  3impa  1099  exp516  1124  r19.29af2  2452  mpteqb  5261  dffo3  5314  fconstfvm  5379  fliftfun  5436  tfrlem1  5923  tfrlem9  5935  nnsucsssuc  6071  nnaordex  6100  diffifi  6351  prarloclemup  6591  genpcdl  6615  genpcuu  6616  recexap  7632  zaddcllemneg  8282  zdiv  8326  uzaddcl  8527  fz0fzelfz0  8982  fz0fzdiffz0  8985  elfzmlbp  8988  difelfzle  8990  fzo1fzo0n0  9037  ssfzo12bi  9079  expivallem  9230  expcllem  9240  expap0  9259  mulexp  9268  cjexp  9467  absexp  9649