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  5727  dffo3  5784  fconstfvm  5861  fliftfun  5926  tfrlem1  6460  tfrlem9  6471  tfr1onlemaccex  6500  tfrcllemaccex  6513  tfrcl  6516  nnsucsssuc  6646  nnaordex  6682  diffifi  7064  fidcenumlemrk  7129  fidcenumlemr  7130  nninfninc  7298  nnnninfeq  7303  nnnninfeq2  7304  exmidontriimlem4  7414  exmidontriim  7415  prarloclemup  7690  genpcdl  7714  genpcuu  7715  negf1o  8536  recexap  8808  zaddcllemneg  9493  zdiv  9543  uzaddcl  9789  fz0fzelfz0  10331  fz0fzdiffz0  10334  elfzmlbp  10336  difelfzle  10338  fzo1fzo0n0  10391  elincfzoext  10407  ssfzo12bi  10439  exfzdc  10454  zsupcllemstep  10457  modfzo0difsn  10625  frecuzrdgg  10646  seq3val  10690  seqvalcd  10691  seqf1og  10751  exp3vallem  10770  expcllem  10780  expap0  10799  mulexp  10808  swrdnd  11199  swrdswrdlem  11244  swrdswrd  11245  pfxccat3  11274  reuccatpfxs1  11287  cjexp  11412  absexp  11598  fimaxre2  11746  summodc  11902  fsum2d  11954  modfsummod  11977  binom  12003  clim2prod  12058  fprod2d  12142  efexp  12201  demoivreALT  12293  divconjdvds  12368  addmodlteqALT  12378  divalglemeunn  12440  divalglemeuneg  12442  bezoutlemstep  12526  bezoutlemmain  12527  dfgcd2  12543  pw2dvdslemn  12695  oddprmdvds  12885  sgrpidmndm  13461  gsumfzz  13536  srgmulgass  13960  ringinvnzdiv  14021  lmodvsmmulgdi  14295  topbas  14749  cnplimclemr  15351  limccnp2lem  15358  gausslemma2dlem3  15750  upgriswlkdc  16081  nninfalllem1  16404  nninfsellemdc  16406  nninfsellemqall  16411  isomninnlem  16428  trirec0  16442  ismkvnnlem  16450