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  6584  tfrlem9  6595  tfr1onlemaccex  6624  tfrcllemaccex  6637  tfrcl  6640  nnsucsssuc  6770  nnaordex  6806  diffifi  7204  fidcenumlemrk  7278  fidcenumlemr  7279  nninfninc  7470  nnnninfeq  7475  nnnninfeq2  7476  exmidontriimlem4  7587  exmidontriim  7588  prarloclemup  7869  genpcdl  7893  genpcuu  7894  negf1o  8717  recexap  8990  zaddcllemneg  9693  zdiv  9745  uzaddcl  10002  fz0fzelfz0  10551  fz0fzdiffz0  10554  elfzmlbp  10556  difelfzle  10558  fzo1fzo0n0  10612  elincfzoext  10628  ssfzo12bi  10660  exfzdc  10676  zsupcllemstep  10679  modfzo0difsn  10853  frecuzrdgg  10874  seq3val  10918  seqvalcd  10919  seqf1og  10979  exp3vallem  10998  expcllem  11008  expap0  11027  mulexp  11036  swrdnd  11453  swrdswrdlem  11498  swrdswrd  11499  pfxccat3  11528  reuccatpfxs1  11541  cjexp  11680  absexp  11868  fimaxre2  12016  summodc  12175  fsum2d  12227  modfsummod  12250  binom  12276  clim2prod  12331  fprod2d  12415  efexp  12474  demoivreALT  12566  divconjdvds  12641  addmodlteqALT  12651  divalglemeunn  12713  divalglemeuneg  12715  bezoutlemstep  12799  bezoutlemmain  12800  dfgcd2  12816  pwbdvdslemn  12969  oddprmdvds  13162  sgrpidmndm  13792  srgmulgass  14400  ringinvnzdiv  14462  lmodvsmmulgdi  14769  assamulgscmlem2  15151  topbas  15326  cnplimclemr  15928  limccnp2lem  15935  gausslemma2dlem3  16420  upgriswlkdc  16839  clwwlkccatlem  16879  umgr2cwwk2dif  16903  clwwlknonex2  16918  depindlem2  16986  depindlem3  16987  nninfalllem1  17290  nninfsellemdc  17292  nninfsellemqall  17297  isomninnlem  17318  trirec0  17333  ismkvnnlem  17342