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  572  con4biddc  864  3impa  1220  exp516  1253  rexlimdva2  2653  r19.29af2  2673  disjiun  4083  mpteqb  5737  dffo3  5794  fconstfvm  5872  fliftfun  5937  tfrlem1  6474  tfrlem9  6485  tfr1onlemaccex  6514  tfrcllemaccex  6527  tfrcl  6530  nnsucsssuc  6660  nnaordex  6696  diffifi  7083  fidcenumlemrk  7153  fidcenumlemr  7154  nninfninc  7322  nnnninfeq  7327  nnnninfeq2  7328  exmidontriimlem4  7439  exmidontriim  7440  prarloclemup  7715  genpcdl  7739  genpcuu  7740  negf1o  8561  recexap  8833  zaddcllemneg  9518  zdiv  9568  uzaddcl  9820  fz0fzelfz0  10362  fz0fzdiffz0  10365  elfzmlbp  10367  difelfzle  10369  fzo1fzo0n0  10423  elincfzoext  10439  ssfzo12bi  10471  exfzdc  10487  zsupcllemstep  10490  modfzo0difsn  10658  frecuzrdgg  10679  seq3val  10723  seqvalcd  10724  seqf1og  10784  exp3vallem  10803  expcllem  10813  expap0  10832  mulexp  10841  swrdnd  11244  swrdswrdlem  11289  swrdswrd  11290  pfxccat3  11319  reuccatpfxs1  11332  cjexp  11458  absexp  11644  fimaxre2  11792  summodc  11949  fsum2d  12001  modfsummod  12024  binom  12050  clim2prod  12105  fprod2d  12189  efexp  12248  demoivreALT  12340  divconjdvds  12415  addmodlteqALT  12425  divalglemeunn  12487  divalglemeuneg  12489  bezoutlemstep  12573  bezoutlemmain  12574  dfgcd2  12590  pw2dvdslemn  12742  oddprmdvds  12932  sgrpidmndm  13508  gsumfzz  13583  srgmulgass  14008  ringinvnzdiv  14069  lmodvsmmulgdi  14343  topbas  14797  cnplimclemr  15399  limccnp2lem  15406  gausslemma2dlem3  15798  upgriswlkdc  16217  clwwlkccatlem  16257  umgr2cwwk2dif  16281  clwwlknonex2  16296  depindlem2  16352  depindlem3  16353  nninfalllem1  16636  nninfsellemdc  16638  nninfsellemqall  16643  isomninnlem  16660  trirec0  16674  ismkvnnlem  16682