Theorem 3expia 1184

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

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

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 965

This theorem is referenced by:  mp3an3  1305  3gencl  2723  moi  2871  sotricim  4253  elirr  4464  en2lp  4477  suc11g  4480  3optocl  4625  sefvex  5450  f1oresrab  5593  ovmpos  5902  ov2gf  5903  poxp  6137  brtposg  6159  dfsmo2  6192  smoiun  6206  tfrlemibxssdm  6232  tfr1onlemsucfn  6245  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemaccex  6253  tfr1onlemres  6254  tfrcllemsucfn  6258  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemaccex  6266  tfrcllemres  6267  tfrcl  6269  nnsucsssuc  6396  nnaordi  6412  nnawordex  6432  mapvalg  6560  pmvalg  6561  elmapg  6563  xpdom3m  6736  ordiso  6929  ctssdc  7006  pr2ne  7065  ltbtwnnqq  7247  prarloclem4  7330  addlocpr  7368  1idprl  7422  1idpru  7423  ltexprlemrnd  7437  recexprlemrnd  7461  recexprlem1ssl  7465  recexprlem1ssu  7466  recexprlemss1l  7467  recexprlemss1u  7468  aptisr  7611  axpre-apti  7717  ltxrlt  7854  axapti  7859  lttri3  7868  reapti  8365  apreap  8373  msqge0  8402  mulge0  8405  recexap  8438  mulap0b  8440  lt2msq  8668  zaddcl  9118  zdiv  9163  zextlt  9167  prime  9174  uzind2  9187  fzind  9190  lbzbi  9435  xltneg  9649  xlt2add  9693  iocssre  9766  icossre  9767  iccssre  9768  fzen  9854  rebtwn2zlemshrink  10062  qbtwnxr  10066  ioo0  10068  ioom  10069  ico0  10070  ioc0  10071  expclzaplem  10348  expnegzap  10358  expaddzap  10368  expmulzap  10370  omgadd  10580  shftuz  10621  cau3lem  10918  climuni  11094  efltim  11441  divalgb  11658  ndvdssub  11663  dvdsgcd  11736  lcmgcdlem  11794  qredeu  11814  isprm3  11835  prmdvdsexpr  11864  prmexpb  11865  ctinf  11979  cnntr  12433  cncnp2m  12439  cnptoprest  12447  lmtopcnp  12458  cnmptcom  12506  hmeof1o  12517  blpnf  12608  blssps  12635  blss  12636  blssec  12646  neibl  12699  climcncf  12779  cnplimcim  12844  bj-peano4  13324  triap  13399