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  7309  exmidontriim  7310  prarloclemup  7581  genpcdl  7605  genpcuu  7606  negf1o  8427  recexap  8699  zaddcllemneg  9384  zdiv  9433  uzaddcl  9679  fz0fzelfz0  10221  fz0fzdiffz0  10224  elfzmlbp  10226  difelfzle  10228  fzo1fzo0n0  10278  ssfzo12bi  10320  exfzdc  10335  zsupcllemstep  10338  modfzo0difsn  10506  frecuzrdgg  10527  seq3val  10571  seqvalcd  10572  seqf1og  10632  exp3vallem  10651  expcllem  10661  expap0  10680  mulexp  10689  cjexp  11077  absexp  11263  fimaxre2  11411  summodc  11567  fsum2d  11619  modfsummod  11642  binom  11668  clim2prod  11723  fprod2d  11807  efexp  11866  demoivreALT  11958  divconjdvds  12033  addmodlteqALT  12043  divalglemeunn  12105  divalglemeuneg  12107  bezoutlemstep  12191  bezoutlemmain  12192  dfgcd2  12208  pw2dvdslemn  12360  oddprmdvds  12550  sgrpidmndm  13124  gsumfzz  13199  srgmulgass  13623  ringinvnzdiv  13684  lmodvsmmulgdi  13957  topbas  14411  cnplimclemr  15013  limccnp2lem  15020  gausslemma2dlem3  15412  nninfalllem1  15763  nninfsellemdc  15765  nninfsellemqall  15770  isomninnlem  15787  trirec0  15801  ismkvnnlem  15809