Theorem 3expb 1204

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  3adant3r1  1212  3adant3r2  1213  3adant3r3  1214  3adant1l  1230  3adant1r  1231  mp3an1  1324  soinxp  4690  sotri  5016  fnfco  5382  mpoeq3dva  5929  fovcdmda  6008  ovelrn  6013  fnmpoovd  6206  nnmsucr  6479  fidifsnid  6861  exmidpw  6898  undiffi  6914  fidcenumlemim  6941  ltpopr  7569  ltexprlemdisj  7580  recexprlemdisj  7604  mul4  8063  add4  8092  2addsub  8145  addsubeq4  8146  subadd4  8175  muladd  8315  ltleadd  8377  divmulap  8605  divap0  8614  div23ap  8621  div12ap  8624  divsubdirap  8638  divcanap5  8644  divmuleqap  8647  divcanap6  8649  divdiv32ap  8650  div2subap  8767  letrp1  8778  lemul12b  8791  lediv1  8799  cju  8891  nndivre  8928  nndivtr  8934  nn0addge1  9195  nn0addge2  9196  peano2uz2  9333  uzind  9337  uzind3  9339  fzind  9341  fnn0ind  9342  uzind4  9561  qre  9598  irrmul  9620  rpdivcl  9650  rerpdivcl  9655  iccshftr  9965  iccshftl  9967  iccdil  9969  icccntr  9971  fzaddel  10029  fzrev  10054  frec2uzf1od  10376  expdivap  10541  2shfti  10808  iooinsup  11253  isermulc2  11316  dvds2add  11800  dvds2sub  11801  dvdstr  11803  alzdvds  11827  divalg2  11898  lcmgcdlem  12044  lcmgcdeq  12050  isprm6  12114  pcqcl  12273  mgmplusf  12660  grprinvd  12680  ismndd  12713  idmhm  12732  submid  12739  0mhm  12744  mhmco  12745  mhmima  12746  grpinvcnv  12808  grpinvnzcl  12812  grpsubf  12819  mhmfmhm  12851  mulgnnsubcl  12865  mulgnn0z  12879  mulgnndir  12881  srgfcl  12962  srgmulgass  12978  srglmhm  12982  srgrmhm  12983  opprringbg  13054  mulgass3  13058  tgclb  13145  topbas  13147  neissex  13245  cnpnei  13299  txcnp  13351  psmetxrge0  13412  psmetlecl  13414  xmetlecl  13447  xmettpos  13450  elbl3ps  13474  elbl3  13475  metss  13574  comet  13579  bdxmet  13581  bdmet  13582  bl2ioo  13622  divcnap  13635  cncfcdm  13649  divccncfap  13657  dvrecap  13757  cosz12  13781