Theorem exp31 350

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

Syntax hints:   → wi 4   ∧ wa 101

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

This theorem is referenced by:  exp41  356  exp42  357  expl  364  exbiri  368  anasss  385  an31s  512  con4biddc  765  3impa  1110  exp516  1135  r19.29af2  2469  mpteqb  5288  dffo3  5341  fconstfvm  5406  fliftfun  5463  tfrlem1  5953  tfrlem9  5965  nnsucsssuc  6101  nnaordex  6130  diffifi  6381  prarloclemup  6650  genpcdl  6674  genpcuu  6675  recexap  7707  zaddcllemneg  8340  zdiv  8385  uzaddcl  8624  fz0fzelfz0  9085  fz0fzdiffz0  9088  elfzmlbp  9091  difelfzle  9093  fzo1fzo0n0  9140  ssfzo12bi  9182  modfzo0difsn  9344  expivallem  9420  expcllem  9430  expap0  9449  mulexp  9458  cjexp  9720  absexp  9905  divconjdvds  10160  addmodlteqALT  10170  pw2dvdslemn  10232