Theorem 3expb 1150

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expb	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3expb

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1148	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 255	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 932

This theorem is referenced by:  3adant3r1  1158  3adant3r2  1159  3adant3r3  1160  3adant1l  1176  3adant1r  1177  mp3an1  1270  soinxp  4547  sotri  4870  fnfco  5233  mpoeq3dva  5767  fovrnda  5846  ovelrn  5851  grprinvd  5898  fnmpoovd  6042  nnmsucr  6314  fidifsnid  6694  exmidpw  6731  undiffi  6742  fidcenumlemim  6768  ltpopr  7304  ltexprlemdisj  7315  recexprlemdisj  7339  mul4  7765  add4  7794  2addsub  7847  addsubeq4  7848  subadd4  7877  muladd  8013  ltleadd  8075  divmulap  8296  divap0  8305  div23ap  8312  div12ap  8315  divsubdirap  8329  divcanap5  8335  divmuleqap  8338  divcanap6  8340  divdiv32ap  8341  div2subap  8457  letrp1  8464  lemul12b  8477  lediv1  8485  cju  8577  nndivre  8614  nndivtr  8620  nn0addge1  8875  nn0addge2  8876  peano2uz2  9010  uzind  9014  uzind3  9016  fzind  9018  fnn0ind  9019  uzind4  9233  qre  9267  irrmul  9289  rpdivcl  9316  rerpdivcl  9321  iccshftr  9618  iccshftl  9620  iccdil  9622  icccntr  9624  fzaddel  9680  fzrev  9705  frec2uzf1od  10020  expdivap  10185  2shfti  10444  iooinsup  10885  isermulc2  10948  dvds2add  11322  dvds2sub  11323  dvdstr  11325  alzdvds  11347  divalg2  11418  lcmgcdlem  11551  lcmgcdeq  11557  isprm6  11618  tgclb  12016  topbas  12018  neissex  12116  cnpnei  12169  txcnp  12221  psmetxrge0  12260  psmetlecl  12262  xmetlecl  12295  xmettpos  12298  elbl3ps  12322  elbl3  12323  metss  12422  comet  12427  bdxmet  12429  bdmet  12430  bl2ioo  12461  cncffvrn  12482  divccncfap  12490