Theorem 3expb 1182

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 1180	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 255	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:  3adant3r1  1190  3adant3r2  1191  3adant3r3  1192  3adant1l  1208  3adant1r  1209  mp3an1  1302  soinxp  4609  sotri  4934  fnfco  5297  mpoeq3dva  5835  fovrnda  5914  ovelrn  5919  grprinvd  5966  fnmpoovd  6112  nnmsucr  6384  fidifsnid  6765  exmidpw  6802  undiffi  6813  fidcenumlemim  6840  ltpopr  7403  ltexprlemdisj  7414  recexprlemdisj  7438  mul4  7894  add4  7923  2addsub  7976  addsubeq4  7977  subadd4  8006  muladd  8146  ltleadd  8208  divmulap  8435  divap0  8444  div23ap  8451  div12ap  8454  divsubdirap  8468  divcanap5  8474  divmuleqap  8477  divcanap6  8479  divdiv32ap  8480  div2subap  8596  letrp1  8606  lemul12b  8619  lediv1  8627  cju  8719  nndivre  8756  nndivtr  8762  nn0addge1  9023  nn0addge2  9024  peano2uz2  9158  uzind  9162  uzind3  9164  fzind  9166  fnn0ind  9167  uzind4  9383  qre  9417  irrmul  9439  rpdivcl  9467  rerpdivcl  9472  iccshftr  9777  iccshftl  9779  iccdil  9781  icccntr  9783  fzaddel  9839  fzrev  9864  frec2uzf1od  10179  expdivap  10344  2shfti  10603  iooinsup  11046  isermulc2  11109  dvds2add  11527  dvds2sub  11528  dvdstr  11530  alzdvds  11552  divalg2  11623  lcmgcdlem  11758  lcmgcdeq  11764  isprm6  11825  tgclb  12234  topbas  12236  neissex  12334  cnpnei  12388  txcnp  12440  psmetxrge0  12501  psmetlecl  12503  xmetlecl  12536  xmettpos  12539  elbl3ps  12563  elbl3  12564  metss  12663  comet  12668  bdxmet  12670  bdmet  12671  bl2ioo  12711  divcnap  12724  cncffvrn  12738  divccncfap  12746  dvrecap  12846  cosz12  12861