Theorem 3expb 1140

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 1138	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 253	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 920

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  3adant3r1  1148  3adant3r2  1149  3adant3r3  1150  3adant1l  1162  3adant1r  1163  mp3an1  1256  soinxp  4430  sotri  4744  fnfco  5090  mpt2eq3dva  5594  fovrnda  5669  ovelrn  5674  grprinvd  5721  nnmsucr  6125  ltpopr  6836  ltexprlemdisj  6847  recexprlemdisj  6871  mul4  7296  add4  7325  2addsub  7378  addsubeq4  7379  subadd4  7408  muladd  7544  ltleadd  7606  divmulap  7819  divap0  7828  div23ap  7835  div12ap  7838  divsubdirap  7852  divcanap5  7858  divmuleqap  7861  divcanap6  7863  divdiv32ap  7864  letrp1  7982  lemul12b  7995  lediv1  8003  cju  8094  nndivre  8130  nndivtr  8136  nn0addge1  8390  nn0addge2  8391  peano2uz2  8524  uzind  8528  uzind3  8530  fzind  8532  fnn0ind  8533  uzind4  8746  qre  8780  irrmul  8802  rpdivcl  8829  rerpdivcl  8834  iccshftr  9081  iccshftl  9083  iccdil  9085  icccntr  9087  fzaddel  9142  fzrev  9166  frec2uzf1od  9477  expdivap  9613  2shfti  9846  iisermulc2  10305  dvds2add  10363  dvds2sub  10364  dvdstr  10366  alzdvds  10388  divalg2  10459  lcmgcdlem  10592  lcmgcdeq  10598  isprm6  10659