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 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  exp41  370  exp42  371  expl  378  exbiri  382  anasss  403  an31s  576  con4biddc  869  3impa  1225  exp516  1258  rexlimdva2  2671  r19.29af2  2691  disjiun  4125  mpteqb  5799  dffo3  5858  fconstfvm  5936  fliftfun  6005  elabreximd  6360  tfrlem1  6583  tfrlem9  6594  tfr1onlemaccex  6623  tfrcllemaccex  6636  tfrcl  6639  nnsucsssuc  6769  nnaordex  6805  diffifi  7203  fidcenumlemrk  7277  fidcenumlemr  7278  nninfninc  7470  nnnninfeq  7475  nnnninfeq2  7476  exmidontriimlem4  7587  exmidontriim  7588  prarloclemup  7869  genpcdl  7893  genpcuu  7894  negf1o  8717  recexap  8990  zaddcllemneg  9695  zdiv  9746  uzaddcl  10003  fz0fzelfz0  10552  fz0fzdiffz0  10555  elfzmlbp  10557  difelfzle  10559  fzo1fzo0n0  10613  elincfzoext  10629  ssfzo12bi  10661  exfzdc  10677  zsupcllemstep  10680  modfzo0difsn  10854  frecuzrdgg  10875  seq3val  10919  seqvalcd  10920  seqf1og  10980  exp3vallem  10999  expcllem  11009  expap0  11028  mulexp  11037  swrdnd  11454  swrdswrdlem  11499  swrdswrd  11500  pfxccat3  11529  reuccatpfxs1  11542  cjexp  11681  absexp  11869  fimaxre2  12017  summodc  12176  fsum2d  12228  modfsummod  12251  binom  12277  clim2prod  12332  fprod2d  12416  efexp  12475  demoivreALT  12567  divconjdvds  12642  addmodlteqALT  12652  divalglemeunn  12714  divalglemeuneg  12716  bezoutlemstep  12800  bezoutlemmain  12801  dfgcd2  12817  pwbdvdslemn  12970  oddprmdvds  13163  sgrpidmndm  13793  srgmulgass  14401  ringinvnzdiv  14463  lmodvsmmulgdi  14770  assamulgscmlem2  15152  topbas  15305  cnplimclemr  15907  limccnp2lem  15914  gausslemma2dlem3  16399  upgriswlkdc  16818  clwwlkccatlem  16858  umgr2cwwk2dif  16882  clwwlknonex2  16897  depindlem2  16965  depindlem3  16966  nninfalllem1  17269  nninfsellemdc  17271  nninfsellemqall  17276  isomninnlem  17297  trirec0  17312  ismkvnnlem  17321