Theorem 3expia 1229

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

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

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 1004

This theorem is referenced by:  ad5ant125  1265  mp3an3  1360  3gencl  2834  moi  2986  ifnebibdc  3648  sotricim  4413  elirr  4632  en2lp  4645  suc11g  4648  3optocl  4796  sefvex  5647  f1oresrab  5799  ovmpos  6127  ov2gf  6128  poxp  6376  brtposg  6398  dfsmo2  6431  smoiun  6445  tfrlemibxssdm  6471  tfr1onlemsucfn  6484  tfr1onlemsucaccv  6485  tfr1onlembxssdm  6487  tfr1onlembfn  6488  tfr1onlemaccex  6492  tfr1onlemres  6493  tfrcllemsucfn  6497  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllembfn  6501  tfrcllemaccex  6505  tfrcllemres  6506  tfrcl  6508  nnsucsssuc  6636  nnaordi  6652  nnawordex  6673  mapvalg  6803  pmvalg  6804  elmapg  6806  xpdom3m  6989  ordiso  7199  ctssdc  7276  pr2ne  7361  ltbtwnnqq  7598  prarloclem4  7681  addlocpr  7719  1idprl  7773  1idpru  7774  ltexprlemrnd  7788  recexprlemrnd  7812  recexprlem1ssl  7816  recexprlem1ssu  7817  recexprlemss1l  7818  recexprlemss1u  7819  aptisr  7962  axpre-apti  8068  ltxrlt  8208  axapti  8213  lttri3  8222  reapti  8722  apreap  8730  msqge0  8759  mulge0  8762  recexap  8796  mulap0b  8798  lt2msq  9029  zaddcl  9482  zdiv  9531  zextlt  9535  prime  9542  uzind2  9555  fzind  9558  lbzbi  9807  xltneg  10028  xlt2add  10072  iocssre  10145  icossre  10146  iccssre  10147  fzen  10235  rebtwn2zlemshrink  10468  qbtwnxr  10472  ioo0  10474  ioom  10475  ico0  10476  ioc0  10477  expclzaplem  10780  expnegzap  10790  expaddzap  10800  expmulzap  10802  omgadd  11019  elovmpowrd  11108  ccatopth2  11244  pfxccatin12  11260  shftuz  11323  cau3lem  11620  climuni  11799  efltim  12204  divalgb  12431  ndvdssub  12436  bitsfzo  12461  dvdsgcd  12528  lcmgcdlem  12594  qredeu  12614  isprm3  12635  prmdvdsexpr  12667  prmexpb  12668  fermltl  12751  coprimeprodsq  12775  pythagtrip  12801  pcpremul  12811  pcdvdsb  12838  pc2dvds  12848  4sqlem12  12920  4sqlem18  12926  ctinf  12996  mulgaddcom  13678  ghmrn  13789  dvdsunit  14070  unitmulclb  14072  lmodvsdi  14269  lss0cl  14327  cnntr  14893  cncnp2m  14899  cnptoprest  14907  lmtopcnp  14918  cnmptcom  14966  hmeof1o  14977  blpnf  15068  blssps  15095  blss  15096  blssec  15106  neibl  15159  climcncf  15252  cnplimcim  15335  plyadd  15419  plymul  15420  upgredg2vtx  15940  bj-peano4  16276  triap  16356