Theorem 3expb 1207

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

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

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 983

This theorem is referenced by:  3adant3r1  1215  3adant3r2  1216  3adant3r3  1217  3adant1l  1233  3adant1r  1234  mp3an1  1337  soinxp  4753  sotri  5087  fnfco  5462  mpoeq3dva  6022  fovcdmda  6103  ovelrn  6108  fnmpoovd  6314  nnmsucr  6587  fidifsnid  6983  exmidpw  7020  undiffi  7037  fidcenumlemim  7069  ltpopr  7728  ltexprlemdisj  7739  recexprlemdisj  7763  mul4  8224  add4  8253  2addsub  8306  addsubeq4  8307  subadd4  8336  muladd  8476  ltleadd  8539  divmulap  8768  divap0  8777  div23ap  8784  div12ap  8787  divsubdirap  8801  divcanap5  8807  divmuleqap  8810  divcanap6  8812  divdiv32ap  8813  div2subap  8930  letrp1  8941  lemul12b  8954  lediv1  8962  cju  9054  nndivre  9092  nndivtr  9098  nn0addge1  9361  nn0addge2  9362  peano2uz2  9500  uzind  9504  uzind3  9506  fzind  9508  fnn0ind  9509  uzind4  9729  qre  9766  irrmul  9788  rpdivcl  9821  rerpdivcl  9826  iccshftr  10136  iccshftl  10138  iccdil  10140  icccntr  10142  fzaddel  10201  fzrev  10226  frec2uzf1od  10573  expdivap  10757  fundm2domnop0  11012  swrdwrdsymbg  11140  ccatpfx  11177  2shfti  11217  iooinsup  11663  isermulc2  11726  dvds2add  12211  dvds2sub  12212  dvdstr  12214  alzdvds  12240  divalg2  12312  lcmgcdlem  12474  lcmgcdeq  12480  isprm6  12544  pcqcl  12704  mgmplusf  13273  grpinva  13293  ismndd  13344  imasmnd2  13359  idmhm  13376  issubm2  13380  submid  13384  0mhm  13393  resmhm  13394  resmhm2  13395  resmhm2b  13396  mhmco  13397  mhmima  13398  gsumwsubmcl  13403  gsumwmhm  13405  grpinvcnv  13475  grpinvnzcl  13479  grpsubf  13486  imasgrp2  13521  qusgrp2  13524  mhmfmhm  13528  mulgnnsubcl  13545  mulgnn0z  13560  mulgnndir  13562  issubg4m  13604  isnsg3  13618  nsgid  13626  qusadd  13645  ghmmhm  13664  ghmmhmb  13665  idghm  13670  resghm  13671  ghmf1  13684  kerf1ghm  13685  qusghm  13693  ghmfghm  13737  invghm  13740  ablnsg  13745  srgfcl  13810  srgmulgass  13826  srglmhm  13830  srgrmhm  13831  ringlghm  13898  ringrghm  13899  opprringbg  13917  mulgass3  13922  isnzr2  14021  subrngringnsg  14042  issubrng2  14047  issubrg2  14078  domnmuln0  14110  islmodd  14130  lmodscaf  14147  lcomf  14164  rmodislmodlem  14187  issubrgd  14289  qusrhm  14365  qusmul2  14366  crngridl  14367  qusmulrng  14369  znidom  14494  psraddcl  14517  tgclb  14612  topbas  14614  neissex  14712  cnpnei  14766  txcnp  14818  psmetxrge0  14879  psmetlecl  14881  xmetlecl  14914  xmettpos  14917  elbl3ps  14941  elbl3  14942  metss  15041  comet  15046  bdxmet  15048  bdmet  15049  bl2ioo  15097  divcnap  15112  cncfcdm  15129  divccncfap  15137  dvrecap  15260  dvmptfsum  15272  cosz12  15327  gausslemma2dlem1a  15610