Theorem 3expia 1232

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

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

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 1007

This theorem is referenced by:  ad5ant125  1268  mp3an3  1363  3gencl  2850  moi  3003  ifnebibdc  3672  sotricim  4449  elirr  4668  en2lp  4681  suc11g  4684  3optocl  4833  sefvex  5696  f1oresrab  5847  ovmpos  6185  ov2gf  6186  poxp  6441  brtposg  6498  dfsmo2  6531  smoiun  6545  tfrlemibxssdm  6571  tfr1onlemsucfn  6584  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllemsucfn  6597  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemaccex  6605  tfrcllemres  6606  tfrcl  6608  nnsucsssuc  6738  nnaordi  6754  nnawordex  6775  mapvalg  6905  pmvalg  6906  elmapg  6908  xpdom3m  7098  ordiso  7340  ctssdc  7417  pr2ne  7502  ltbtwnnqq  7746  prarloclem4  7829  addlocpr  7867  1idprl  7921  1idpru  7922  ltexprlemrnd  7936  recexprlemrnd  7960  recexprlem1ssl  7964  recexprlem1ssu  7965  recexprlemss1l  7966  recexprlemss1u  7967  aptisr  8110  axpre-apti  8216  ltxrlt  8355  axapti  8360  lttri3  8369  reapti  8870  apreap  8878  msqge0  8907  mulge0  8910  recexap  8944  mulap0b  8946  lt2msq  9177  zaddcl  9634  zdiv  9684  zextlt  9688  prime  9695  uzind2  9708  fzind  9711  lbzbi  9966  xltneg  10188  xlt2add  10232  iocssre  10305  icossre  10306  iccssre  10307  fzen  10397  rebtwn2zlemshrink  10637  qbtwnxr  10641  ioo0  10643  ioom  10644  ico0  10645  ioc0  10646  expclzaplem  10949  expnegzap  10959  expaddzap  10969  expmulzap  10971  omgadd  11191  elovmpowrd  11291  ccatopth2  11434  pfxccatin12  11450  shftuz  11527  cau3lem  11824  climuni  12003  efltim  12409  divalgb  12636  ndvdssub  12641  bitsfzo  12666  dvdsgcd  12733  lcmgcdlem  12799  qredeu  12819  isprm3  12840  prmdvdsexpr  12872  prmexpb  12873  fermltl  12956  coprimeprodsq  12980  pythagtrip  13006  pcpremul  13016  pcdvdsb  13043  pc2dvds  13053  4sqlem12  13125  4sqlem18  13131  ballotfilemirc  13219  ctinf  13265  mulgaddcom  13899  ghmrn  14010  dvdsunit  14357  unitmulclb  14359  lmodvsdi  14585  lss0cl  14643  cnntr  15216  cncnp2m  15222  cnptoprest  15230  lmtopcnp  15241  cnmptcom  15289  hmeof1o  15300  blpnf  15391  blssps  15418  blss  15419  blssec  15429  neibl  15482  climcncf  15575  cnplimcim  15658  plyadd  15742  plymul  15743  upgredg2vtx  16269  bj-peano4  16851  triap  16939