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  6593  genpcdl  6617  genpcuu  6618  recexap  7634  zaddcllemneg  8284  zdiv  8328  uzaddcl  8529  fz0fzelfz0  8984  fz0fzdiffz0  8987  elfzmlbp  8990  difelfzle  8992  fzo1fzo0n0  9039  ssfzo12bi  9081  expivallem  9256  expcllem  9266  expap0  9285  mulexp  9294  cjexp  9493  absexp  9675