Theorem 3expb 1142

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

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

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 924

This theorem is referenced by:  3adant3r1  1150  3adant3r2  1151  3adant3r3  1152  3adant1l  1164  3adant1r  1165  mp3an1  1258  soinxp  4478  sotri  4796  fnfco  5151  mpt2eq3dva  5672  fovrnda  5747  ovelrn  5752  grprinvd  5799  nnmsucr  6205  fidifsnid  6541  exmidpw  6578  undiffi  6589  ltpopr  7101  ltexprlemdisj  7112  recexprlemdisj  7136  mul4  7561  add4  7590  2addsub  7643  addsubeq4  7644  subadd4  7673  muladd  7809  ltleadd  7871  divmulap  8084  divap0  8093  div23ap  8100  div12ap  8103  divsubdirap  8117  divcanap5  8123  divmuleqap  8126  divcanap6  8128  divdiv32ap  8129  letrp1  8247  lemul12b  8260  lediv1  8268  cju  8359  nndivre  8395  nndivtr  8401  nn0addge1  8655  nn0addge2  8656  peano2uz2  8789  uzind  8793  uzind3  8795  fzind  8797  fnn0ind  8798  uzind4  9011  qre  9045  irrmul  9067  rpdivcl  9094  rerpdivcl  9099  iccshftr  9346  iccshftl  9348  iccdil  9350  icccntr  9352  fzaddel  9407  fzrev  9431  frec2uzf1od  9744  expdivap  9926  2shfti  10183  iisermulc2  10644  dvds2add  10755  dvds2sub  10756  dvdstr  10758  alzdvds  10780  divalg2  10851  lcmgcdlem  10984  lcmgcdeq  10990  isprm6  11051