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  5796  dffo3  5855  fconstfvm  5933  fliftfun  6002  elabreximd  6356  tfrlem1  6579  tfrlem9  6590  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfrcl  6635  nnsucsssuc  6765  nnaordex  6801  diffifi  7198  fidcenumlemrk  7271  fidcenumlemr  7272  nninfninc  7463  nnnninfeq  7468  nnnninfeq2  7469  exmidontriimlem4  7580  exmidontriim  7581  prarloclemup  7862  genpcdl  7886  genpcuu  7887  negf1o  8709  recexap  8982  zaddcllemneg  9685  zdiv  9736  uzaddcl  9988  fz0fzelfz0  10536  fz0fzdiffz0  10539  elfzmlbp  10541  difelfzle  10543  fzo1fzo0n0  10597  elincfzoext  10613  ssfzo12bi  10645  exfzdc  10661  zsupcllemstep  10664  modfzo0difsn  10834  frecuzrdgg  10855  seq3val  10899  seqvalcd  10900  seqf1og  10960  exp3vallem  10979  expcllem  10989  expap0  11008  mulexp  11017  swrdnd  11433  swrdswrdlem  11478  swrdswrd  11479  pfxccat3  11508  reuccatpfxs1  11521  cjexp  11660  absexp  11847  fimaxre2  11995  summodc  12152  fsum2d  12204  modfsummod  12227  binom  12253  clim2prod  12308  fprod2d  12392  efexp  12451  demoivreALT  12543  divconjdvds  12618  addmodlteqALT  12628  divalglemeunn  12690  divalglemeuneg  12692  bezoutlemstep  12776  bezoutlemmain  12777  dfgcd2  12793  pw2dvdslemn  12945  oddprmdvds  13135  sgrpidmndm  13735  srgmulgass  14295  ringinvnzdiv  14357  lmodvsmmulgdi  14662  assamulgscmlem2  15044  topbas  15170  cnplimclemr  15772  limccnp2lem  15779  gausslemma2dlem3  16194  upgriswlkdc  16613  clwwlkccatlem  16653  umgr2cwwk2dif  16677  clwwlknonex2  16692  depindlem2  16760  depindlem3  16761  nninfalllem1  17063  nninfsellemdc  17065  nninfsellemqall  17070  isomninnlem  17091  trirec0  17105  ismkvnnlem  17114