Theorem exp31 364

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  exp41  370  exp42  371  expl  378  exbiri  382  anasss  399  an31s  570  con4biddc  862  3impa  1218  exp516  1251  rexlimdva2  2651  r19.29af2  2671  disjiun  4078  mpteqb  5730  dffo3  5787  fconstfvm  5864  fliftfun  5929  tfrlem1  6465  tfrlem9  6476  tfr1onlemaccex  6505  tfrcllemaccex  6518  tfrcl  6521  nnsucsssuc  6651  nnaordex  6687  diffifi  7069  fidcenumlemrk  7137  fidcenumlemr  7138  nninfninc  7306  nnnninfeq  7311  nnnninfeq2  7312  exmidontriimlem4  7422  exmidontriim  7423  prarloclemup  7698  genpcdl  7722  genpcuu  7723  negf1o  8544  recexap  8816  zaddcllemneg  9501  zdiv  9551  uzaddcl  9798  fz0fzelfz0  10340  fz0fzdiffz0  10343  elfzmlbp  10345  difelfzle  10347  fzo1fzo0n0  10400  elincfzoext  10416  ssfzo12bi  10448  exfzdc  10463  zsupcllemstep  10466  modfzo0difsn  10634  frecuzrdgg  10655  seq3val  10699  seqvalcd  10700  seqf1og  10760  exp3vallem  10779  expcllem  10789  expap0  10808  mulexp  10817  swrdnd  11212  swrdswrdlem  11257  swrdswrd  11258  pfxccat3  11287  reuccatpfxs1  11300  cjexp  11425  absexp  11611  fimaxre2  11759  summodc  11915  fsum2d  11967  modfsummod  11990  binom  12016  clim2prod  12071  fprod2d  12155  efexp  12214  demoivreALT  12306  divconjdvds  12381  addmodlteqALT  12391  divalglemeunn  12453  divalglemeuneg  12455  bezoutlemstep  12539  bezoutlemmain  12540  dfgcd2  12556  pw2dvdslemn  12708  oddprmdvds  12898  sgrpidmndm  13474  gsumfzz  13549  srgmulgass  13973  ringinvnzdiv  14034  lmodvsmmulgdi  14308  topbas  14762  cnplimclemr  15364  limccnp2lem  15371  gausslemma2dlem3  15763  upgriswlkdc  16132  clwwlkccatlem  16169  umgr2cwwk2dif  16192  nninfalllem1  16488  nninfsellemdc  16490  nninfsellemqall  16495  isomninnlem  16512  trirec0  16526  ismkvnnlem  16534