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  859  3impa  1197  exp516  1230  rexlimdva2  2627  r19.29af2  2647  disjiun  4043  mpteqb  5680  dffo3  5737  fconstfvm  5812  fliftfun  5875  tfrlem1  6404  tfrlem9  6415  tfr1onlemaccex  6444  tfrcllemaccex  6457  tfrcl  6460  nnsucsssuc  6588  nnaordex  6624  diffifi  7003  fidcenumlemrk  7068  fidcenumlemr  7069  nninfninc  7237  nnnninfeq  7242  nnnninfeq2  7243  exmidontriimlem4  7349  exmidontriim  7350  prarloclemup  7621  genpcdl  7645  genpcuu  7646  negf1o  8467  recexap  8739  zaddcllemneg  9424  zdiv  9474  uzaddcl  9720  fz0fzelfz0  10262  fz0fzdiffz0  10265  elfzmlbp  10267  difelfzle  10269  fzo1fzo0n0  10320  elincfzoext  10335  ssfzo12bi  10367  exfzdc  10382  zsupcllemstep  10385  modfzo0difsn  10553  frecuzrdgg  10574  seq3val  10618  seqvalcd  10619  seqf1og  10679  exp3vallem  10698  expcllem  10708  expap0  10727  mulexp  10736  swrdnd  11126  swrdswrdlem  11169  swrdswrd  11170  cjexp  11254  absexp  11440  fimaxre2  11588  summodc  11744  fsum2d  11796  modfsummod  11819  binom  11845  clim2prod  11900  fprod2d  11984  efexp  12043  demoivreALT  12135  divconjdvds  12210  addmodlteqALT  12220  divalglemeunn  12282  divalglemeuneg  12284  bezoutlemstep  12368  bezoutlemmain  12369  dfgcd2  12385  pw2dvdslemn  12537  oddprmdvds  12727  sgrpidmndm  13302  gsumfzz  13377  srgmulgass  13801  ringinvnzdiv  13862  lmodvsmmulgdi  14135  topbas  14589  cnplimclemr  15191  limccnp2lem  15198  gausslemma2dlem3  15590  nninfalllem1  16060  nninfsellemdc  16062  nninfsellemqall  16067  isomninnlem  16084  trirec0  16098  ismkvnnlem  16106