Theorem 3expia 1231

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1004

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

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  ad5ant125  1267  mp3an3  1362  3gencl  2837  moi  2989  ifnebibdc  3651  sotricim  4420  elirr  4639  en2lp  4652  suc11g  4655  3optocl  4804  sefvex  5660  f1oresrab  5812  ovmpos  6144  ov2gf  6145  poxp  6396  brtposg  6419  dfsmo2  6452  smoiun  6466  tfrlemibxssdm  6492  tfr1onlemsucfn  6505  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfr1onlemaccex  6513  tfr1onlemres  6514  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemaccex  6526  tfrcllemres  6527  tfrcl  6529  nnsucsssuc  6659  nnaordi  6675  nnawordex  6696  mapvalg  6826  pmvalg  6827  elmapg  6829  xpdom3m  7017  ordiso  7234  ctssdc  7311  pr2ne  7396  ltbtwnnqq  7634  prarloclem4  7717  addlocpr  7755  1idprl  7809  1idpru  7810  ltexprlemrnd  7824  recexprlemrnd  7848  recexprlem1ssl  7852  recexprlem1ssu  7853  recexprlemss1l  7854  recexprlemss1u  7855  aptisr  7998  axpre-apti  8104  ltxrlt  8244  axapti  8249  lttri3  8258  reapti  8758  apreap  8766  msqge0  8795  mulge0  8798  recexap  8832  mulap0b  8834  lt2msq  9065  zaddcl  9518  zdiv  9567  zextlt  9571  prime  9578  uzind2  9591  fzind  9594  lbzbi  9849  xltneg  10070  xlt2add  10114  iocssre  10187  icossre  10188  iccssre  10189  fzen  10277  rebtwn2zlemshrink  10512  qbtwnxr  10516  ioo0  10518  ioom  10519  ico0  10520  ioc0  10521  expclzaplem  10824  expnegzap  10834  expaddzap  10844  expmulzap  10846  omgadd  11064  elovmpowrd  11154  ccatopth2  11297  pfxccatin12  11313  shftuz  11377  cau3lem  11674  climuni  11853  efltim  12258  divalgb  12485  ndvdssub  12490  bitsfzo  12515  dvdsgcd  12582  lcmgcdlem  12648  qredeu  12668  isprm3  12689  prmdvdsexpr  12721  prmexpb  12722  fermltl  12805  coprimeprodsq  12829  pythagtrip  12855  pcpremul  12865  pcdvdsb  12892  pc2dvds  12902  4sqlem12  12974  4sqlem18  12980  ctinf  13050  mulgaddcom  13732  ghmrn  13843  dvdsunit  14125  unitmulclb  14127  lmodvsdi  14324  lss0cl  14382  cnntr  14948  cncnp2m  14954  cnptoprest  14962  lmtopcnp  14973  cnmptcom  15021  hmeof1o  15032  blpnf  15123  blssps  15150  blss  15151  blssec  15161  neibl  15214  climcncf  15307  cnplimcim  15390  plyadd  15474  plymul  15475  upgredg2vtx  15998  bj-peano4  16550  triap  16633