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  862  3impa  1218  exp516  1251  rexlimdva2  2651  r19.29af2  2671  disjiun  4077  mpteqb  5718  dffo3  5775  fconstfvm  5850  fliftfun  5913  tfrlem1  6444  tfrlem9  6455  tfr1onlemaccex  6484  tfrcllemaccex  6497  tfrcl  6500  nnsucsssuc  6628  nnaordex  6664  diffifi  7044  fidcenumlemrk  7109  fidcenumlemr  7110  nninfninc  7278  nnnninfeq  7283  nnnninfeq2  7284  exmidontriimlem4  7394  exmidontriim  7395  prarloclemup  7670  genpcdl  7694  genpcuu  7695  negf1o  8516  recexap  8788  zaddcllemneg  9473  zdiv  9523  uzaddcl  9769  fz0fzelfz0  10311  fz0fzdiffz0  10314  elfzmlbp  10316  difelfzle  10318  fzo1fzo0n0  10371  elincfzoext  10386  ssfzo12bi  10418  exfzdc  10433  zsupcllemstep  10436  modfzo0difsn  10604  frecuzrdgg  10625  seq3val  10669  seqvalcd  10670  seqf1og  10730  exp3vallem  10749  expcllem  10759  expap0  10778  mulexp  10787  swrdnd  11177  swrdswrdlem  11222  swrdswrd  11223  pfxccat3  11252  reuccatpfxs1  11265  cjexp  11390  absexp  11576  fimaxre2  11724  summodc  11880  fsum2d  11932  modfsummod  11955  binom  11981  clim2prod  12036  fprod2d  12120  efexp  12179  demoivreALT  12271  divconjdvds  12346  addmodlteqALT  12356  divalglemeunn  12418  divalglemeuneg  12420  bezoutlemstep  12504  bezoutlemmain  12505  dfgcd2  12521  pw2dvdslemn  12673  oddprmdvds  12863  sgrpidmndm  13439  gsumfzz  13514  srgmulgass  13938  ringinvnzdiv  13999  lmodvsmmulgdi  14272  topbas  14726  cnplimclemr  15328  limccnp2lem  15335  gausslemma2dlem3  15727  nninfalllem1  16305  nninfsellemdc  16307  nninfsellemqall  16312  isomninnlem  16329  trirec0  16343  ismkvnnlem  16351