Theorem 3expia 1195

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 1192	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 123	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  mp3an3  1316  3gencl  2759  moi  2908  sotricim  4300  elirr  4517  en2lp  4530  suc11g  4533  3optocl  4681  sefvex  5506  f1oresrab  5649  ovmpos  5961  ov2gf  5962  poxp  6196  brtposg  6218  dfsmo2  6251  smoiun  6265  tfrlemibxssdm  6291  tfr1onlemsucfn  6304  tfr1onlemsucaccv  6305  tfr1onlembxssdm  6307  tfr1onlembfn  6308  tfr1onlemaccex  6312  tfr1onlemres  6313  tfrcllemsucfn  6317  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllembfn  6321  tfrcllemaccex  6325  tfrcllemres  6326  tfrcl  6328  nnsucsssuc  6456  nnaordi  6472  nnawordex  6492  mapvalg  6620  pmvalg  6621  elmapg  6623  xpdom3m  6796  ordiso  6997  ctssdc  7074  pr2ne  7144  ltbtwnnqq  7352  prarloclem4  7435  addlocpr  7473  1idprl  7527  1idpru  7528  ltexprlemrnd  7542  recexprlemrnd  7566  recexprlem1ssl  7570  recexprlem1ssu  7571  recexprlemss1l  7572  recexprlemss1u  7573  aptisr  7716  axpre-apti  7822  ltxrlt  7960  axapti  7965  lttri3  7974  reapti  8473  apreap  8481  msqge0  8510  mulge0  8513  recexap  8546  mulap0b  8548  lt2msq  8777  zaddcl  9227  zdiv  9275  zextlt  9279  prime  9286  uzind2  9299  fzind  9302  lbzbi  9550  xltneg  9768  xlt2add  9812  iocssre  9885  icossre  9886  iccssre  9887  fzen  9974  rebtwn2zlemshrink  10185  qbtwnxr  10189  ioo0  10191  ioom  10192  ico0  10193  ioc0  10194  expclzaplem  10475  expnegzap  10485  expaddzap  10495  expmulzap  10497  omgadd  10711  shftuz  10755  cau3lem  11052  climuni  11230  efltim  11635  divalgb  11858  ndvdssub  11863  dvdsgcd  11941  lcmgcdlem  12005  qredeu  12025  isprm3  12046  prmdvdsexpr  12078  prmexpb  12079  fermltl  12162  coprimeprodsq  12185  pythagtrip  12211  pcpremul  12221  pcdvdsb  12247  pc2dvds  12257  ctinf  12359  cnntr  12825  cncnp2m  12831  cnptoprest  12839  lmtopcnp  12850  cnmptcom  12898  hmeof1o  12909  blpnf  13000  blssps  13027  blss  13028  blssec  13038  neibl  13091  climcncf  13171  cnplimcim  13236  bj-peano4  13797  triap  13868