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  858  3impa  1196  exp516  1229  rexlimdva2  2617  r19.29af2  2637  disjiun  4029  mpteqb  5655  dffo3  5712  fconstfvm  5783  fliftfun  5846  tfrlem1  6375  tfrlem9  6386  tfr1onlemaccex  6415  tfrcllemaccex  6428  tfrcl  6431  nnsucsssuc  6559  nnaordex  6595  diffifi  6964  fidcenumlemrk  7029  fidcenumlemr  7030  nninfninc  7198  nnnninfeq  7203  nnnninfeq2  7204  exmidontriimlem4  7307  exmidontriim  7308  prarloclemup  7579  genpcdl  7603  genpcuu  7604  negf1o  8425  recexap  8697  zaddcllemneg  9382  zdiv  9431  uzaddcl  9677  fz0fzelfz0  10219  fz0fzdiffz0  10222  elfzmlbp  10224  difelfzle  10226  fzo1fzo0n0  10276  ssfzo12bi  10318  exfzdc  10333  zsupcllemstep  10336  modfzo0difsn  10504  frecuzrdgg  10525  seq3val  10569  seqvalcd  10570  seqf1og  10630  exp3vallem  10649  expcllem  10659  expap0  10678  mulexp  10687  cjexp  11075  absexp  11261  fimaxre2  11409  summodc  11565  fsum2d  11617  modfsummod  11640  binom  11666  clim2prod  11721  fprod2d  11805  efexp  11864  demoivreALT  11956  divconjdvds  12031  addmodlteqALT  12041  divalglemeunn  12103  divalglemeuneg  12105  bezoutlemstep  12189  bezoutlemmain  12190  dfgcd2  12206  pw2dvdslemn  12358  oddprmdvds  12548  sgrpidmndm  13122  gsumfzz  13197  srgmulgass  13621  ringinvnzdiv  13682  lmodvsmmulgdi  13955  topbas  14387  cnplimclemr  14989  limccnp2lem  14996  gausslemma2dlem3  15388  nninfalllem1  15739  nninfsellemdc  15741  nninfsellemqall  15746  isomninnlem  15761  trirec0  15775  ismkvnnlem  15783