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  4415  elirr  4634  en2lp  4647  suc11g  4650  3optocl  4799  sefvex  5653  f1oresrab  5805  ovmpos  6137  ov2gf  6138  poxp  6389  brtposg  6411  dfsmo2  6444  smoiun  6458  tfrlemibxssdm  6484  tfr1onlemsucfn  6497  tfr1onlemsucaccv  6498  tfr1onlembxssdm  6500  tfr1onlembfn  6501  tfr1onlemaccex  6505  tfr1onlemres  6506  tfrcllemsucfn  6510  tfrcllemsucaccv  6511  tfrcllembxssdm  6513  tfrcllembfn  6514  tfrcllemaccex  6518  tfrcllemres  6519  tfrcl  6521  nnsucsssuc  6651  nnaordi  6667  nnawordex  6688  mapvalg  6818  pmvalg  6819  elmapg  6821  xpdom3m  7006  ordiso  7219  ctssdc  7296  pr2ne  7381  ltbtwnnqq  7618  prarloclem4  7701  addlocpr  7739  1idprl  7793  1idpru  7794  ltexprlemrnd  7808  recexprlemrnd  7832  recexprlem1ssl  7836  recexprlem1ssu  7837  recexprlemss1l  7838  recexprlemss1u  7839  aptisr  7982  axpre-apti  8088  ltxrlt  8228  axapti  8233  lttri3  8242  reapti  8742  apreap  8750  msqge0  8779  mulge0  8782  recexap  8816  mulap0b  8818  lt2msq  9049  zaddcl  9502  zdiv  9551  zextlt  9555  prime  9562  uzind2  9575  fzind  9578  lbzbi  9828  xltneg  10049  xlt2add  10093  iocssre  10166  icossre  10167  iccssre  10168  fzen  10256  rebtwn2zlemshrink  10490  qbtwnxr  10494  ioo0  10496  ioom  10497  ico0  10498  ioc0  10499  expclzaplem  10802  expnegzap  10812  expaddzap  10822  expmulzap  10824  omgadd  11041  elovmpowrd  11131  ccatopth2  11270  pfxccatin12  11286  shftuz  11349  cau3lem  11646  climuni  11825  efltim  12230  divalgb  12457  ndvdssub  12462  bitsfzo  12487  dvdsgcd  12554  lcmgcdlem  12620  qredeu  12640  isprm3  12661  prmdvdsexpr  12693  prmexpb  12694  fermltl  12777  coprimeprodsq  12801  pythagtrip  12827  pcpremul  12837  pcdvdsb  12864  pc2dvds  12874  4sqlem12  12946  4sqlem18  12952  ctinf  13022  mulgaddcom  13704  ghmrn  13815  dvdsunit  14097  unitmulclb  14099  lmodvsdi  14296  lss0cl  14354  cnntr  14920  cncnp2m  14926  cnptoprest  14934  lmtopcnp  14945  cnmptcom  14993  hmeof1o  15004  blpnf  15095  blssps  15122  blss  15123  blssec  15133  neibl  15186  climcncf  15279  cnplimcim  15362  plyadd  15446  plymul  15447  upgredg2vtx  15967  bj-peano4  16427  triap  16511