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  572  con4biddc  865  3impa  1221  exp516  1254  rexlimdva2  2665  r19.29af2  2685  disjiun  4109  mpteqb  5773  dffo3  5829  fconstfvm  5907  fliftfun  5975  elabreximd  6329  tfrlem1  6552  tfrlem9  6563  tfr1onlemaccex  6592  tfrcllemaccex  6605  tfrcl  6608  nnsucsssuc  6738  nnaordex  6774  diffifi  7164  fidcenumlemrk  7237  fidcenumlemr  7238  nninfninc  7427  nnnninfeq  7432  nnnninfeq2  7433  exmidontriimlem4  7544  exmidontriim  7545  prarloclemup  7826  genpcdl  7850  genpcuu  7851  negf1o  8672  recexap  8944  zaddcllemneg  9633  zdiv  9684  uzaddcl  9936  fz0fzelfz0  10483  fz0fzdiffz0  10486  elfzmlbp  10488  difelfzle  10490  fzo1fzo0n0  10544  elincfzoext  10560  ssfzo12bi  10592  exfzdc  10608  zsupcllemstep  10611  modfzo0difsn  10781  frecuzrdgg  10802  seq3val  10846  seqvalcd  10847  seqf1og  10907  exp3vallem  10926  expcllem  10936  expap0  10955  mulexp  10964  swrdnd  11376  swrdswrdlem  11421  swrdswrd  11422  pfxccat3  11451  reuccatpfxs1  11464  cjexp  11603  absexp  11789  fimaxre2  11937  summodc  12094  fsum2d  12146  modfsummod  12169  binom  12195  clim2prod  12250  fprod2d  12334  efexp  12393  demoivreALT  12485  divconjdvds  12560  addmodlteqALT  12570  divalglemeunn  12632  divalglemeuneg  12634  bezoutlemstep  12718  bezoutlemmain  12719  dfgcd2  12735  pw2dvdslemn  12887  oddprmdvds  13077  sgrpidmndm  13717  gsumfzz  13792  srgmulgass  14217  ringinvnzdiv  14278  lmodvsmmulgdi  14583  topbas  15044  cnplimclemr  15646  limccnp2lem  15653  gausslemma2dlem3  16048  upgriswlkdc  16467  clwwlkccatlem  16507  umgr2cwwk2dif  16531  clwwlknonex2  16546  depindlem2  16614  depindlem3  16615  nninfalllem1  16898  nninfsellemdc  16900  nninfsellemqall  16905  isomninnlem  16926  trirec0  16940  ismkvnnlem  16949