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  4081  mpteqb  5733  dffo3  5790  fconstfvm  5867  fliftfun  5932  tfrlem1  6469  tfrlem9  6480  tfr1onlemaccex  6509  tfrcllemaccex  6522  tfrcl  6525  nnsucsssuc  6655  nnaordex  6691  diffifi  7078  fidcenumlemrk  7147  fidcenumlemr  7148  nninfninc  7316  nnnninfeq  7321  nnnninfeq2  7322  exmidontriimlem4  7432  exmidontriim  7433  prarloclemup  7708  genpcdl  7732  genpcuu  7733  negf1o  8554  recexap  8826  zaddcllemneg  9511  zdiv  9561  uzaddcl  9813  fz0fzelfz0  10355  fz0fzdiffz0  10358  elfzmlbp  10360  difelfzle  10362  fzo1fzo0n0  10415  elincfzoext  10431  ssfzo12bi  10463  exfzdc  10479  zsupcllemstep  10482  modfzo0difsn  10650  frecuzrdgg  10671  seq3val  10715  seqvalcd  10716  seqf1og  10776  exp3vallem  10795  expcllem  10805  expap0  10824  mulexp  10833  swrdnd  11233  swrdswrdlem  11278  swrdswrd  11279  pfxccat3  11308  reuccatpfxs1  11321  cjexp  11447  absexp  11633  fimaxre2  11781  summodc  11937  fsum2d  11989  modfsummod  12012  binom  12038  clim2prod  12093  fprod2d  12177  efexp  12236  demoivreALT  12328  divconjdvds  12403  addmodlteqALT  12413  divalglemeunn  12475  divalglemeuneg  12477  bezoutlemstep  12561  bezoutlemmain  12562  dfgcd2  12578  pw2dvdslemn  12730  oddprmdvds  12920  sgrpidmndm  13496  gsumfzz  13571  srgmulgass  13995  ringinvnzdiv  14056  lmodvsmmulgdi  14330  topbas  14784  cnplimclemr  15386  limccnp2lem  15393  gausslemma2dlem3  15785  upgriswlkdc  16171  clwwlkccatlem  16209  umgr2cwwk2dif  16233  clwwlknonex2  16248  nninfalllem1  16560  nninfsellemdc  16562  nninfsellemqall  16567  isomninnlem  16584  trirec0  16598  ismkvnnlem  16606