Theorem 3expia 1106

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expia	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1103	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 115	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  mp3an3  1221  3gencl  2588  moi  2724  sotricim  4060  elirr  4266  en2lp  4278  suc11g  4281  3optocl  4418  sefvex  5196  f1oresrab  5329  ovmpt2s  5624  ov2gf  5625  poxp  5853  brtposg  5869  dfsmo2  5902  smoiun  5916  tfrlemibxssdm  5941  nnsucsssuc  6071  nnaordi  6081  nnawordex  6101  xpdom3m  6308  ordiso  6358  ltbtwnnqq  6513  prarloclem4  6596  addlocpr  6634  1idprl  6688  1idpru  6689  ltexprlemrnd  6703  recexprlemrnd  6727  recexprlem1ssl  6731  recexprlem1ssu  6732  recexprlemss1l  6733  recexprlemss1u  6734  aptisr  6863  axpre-apti  6959  ltxrlt  7085  axapti  7090  lttri3  7098  reapti  7570  apreap  7578  msqge0  7607  mulge0  7610  recexap  7634  mulap0b  7636  lt2msq  7852  zaddcl  8285  zdiv  8328  zextlt  8332  prime  8337  uzind2  8350  fzind  8353  lbzbi  8551  xltneg  8749  iocssre  8822  icossre  8823  iccssre  8824  fzen  8907  qbtwnzlemshrink  9104  rebtwn2zlemshrink  9108  expival  9257  expclzaplem  9279  expnegzap  9289  expaddzap  9299  expmulzap  9301  shftuz  9418  cau3lem  9710  climuni  9814  bj-peano4  10080