Theorem 3expia 1183

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

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

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 964

This theorem is referenced by:  mp3an3  1304  3gencl  2715  moi  2862  sotricim  4240  elirr  4451  en2lp  4464  suc11g  4467  3optocl  4612  sefvex  5435  f1oresrab  5578  ovmpos  5887  ov2gf  5888  poxp  6122  brtposg  6144  dfsmo2  6177  smoiun  6191  tfrlemibxssdm  6217  tfr1onlemsucfn  6230  tfr1onlemsucaccv  6231  tfr1onlembxssdm  6233  tfr1onlembfn  6234  tfr1onlemaccex  6238  tfr1onlemres  6239  tfrcllemsucfn  6243  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  tfrcllembfn  6247  tfrcllemaccex  6251  tfrcllemres  6252  tfrcl  6254  nnsucsssuc  6381  nnaordi  6397  nnawordex  6417  mapvalg  6545  pmvalg  6546  elmapg  6548  xpdom3m  6721  ordiso  6914  ctssdc  6991  pr2ne  7041  ltbtwnnqq  7216  prarloclem4  7299  addlocpr  7337  1idprl  7391  1idpru  7392  ltexprlemrnd  7406  recexprlemrnd  7430  recexprlem1ssl  7434  recexprlem1ssu  7435  recexprlemss1l  7436  recexprlemss1u  7437  aptisr  7580  axpre-apti  7686  ltxrlt  7823  axapti  7828  lttri3  7837  reapti  8334  apreap  8342  msqge0  8371  mulge0  8374  recexap  8407  mulap0b  8409  lt2msq  8637  zaddcl  9087  zdiv  9132  zextlt  9136  prime  9143  uzind2  9156  fzind  9159  lbzbi  9401  xltneg  9612  xlt2add  9656  iocssre  9729  icossre  9730  iccssre  9731  fzen  9816  rebtwn2zlemshrink  10024  qbtwnxr  10028  ioo0  10030  ioom  10031  ico0  10032  ioc0  10033  expclzaplem  10310  expnegzap  10320  expaddzap  10330  expmulzap  10332  omgadd  10541  shftuz  10582  cau3lem  10879  climuni  11055  efltim  11393  divalgb  11611  ndvdssub  11616  dvdsgcd  11689  lcmgcdlem  11747  qredeu  11767  isprm3  11788  prmdvdsexpr  11817  prmexpb  11818  ctinf  11932  cnntr  12383  cncnp2m  12389  cnptoprest  12397  lmtopcnp  12408  cnmptcom  12456  hmeof1o  12467  blpnf  12558  blssps  12585  blss  12586  blssec  12596  neibl  12649  climcncf  12729  cnplimcim  12794  bj-peano4  13142  triap  13213