Theorem 3expb 1228

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

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

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 1004

This theorem is referenced by:  3adant3r1  1236  3adant3r2  1237  3adant3r3  1238  3adant1l  1254  3adant1r  1255  mp3an1  1358  soinxp  4789  sotri  5124  fnfco  5502  mpoeq3dva  6074  fovcdmda  6155  ovelrn  6160  fnmpoovd  6367  nnmsucr  6642  fidifsnid  7041  exmidpw  7081  undiffi  7098  fidcenumlemim  7130  ltpopr  7793  ltexprlemdisj  7804  recexprlemdisj  7828  mul4  8289  add4  8318  2addsub  8371  addsubeq4  8372  subadd4  8401  muladd  8541  ltleadd  8604  divmulap  8833  divap0  8842  div23ap  8849  div12ap  8852  divsubdirap  8866  divcanap5  8872  divmuleqap  8875  divcanap6  8877  divdiv32ap  8878  div2subap  8995  letrp1  9006  lemul12b  9019  lediv1  9027  cju  9119  nndivre  9157  nndivtr  9163  nn0addge1  9426  nn0addge2  9427  peano2uz2  9565  uzind  9569  uzind3  9571  fzind  9573  fnn0ind  9574  uzind4  9795  qre  9832  irrmul  9854  rpdivcl  9887  rerpdivcl  9892  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  fzaddel  10267  fzrev  10292  frec2uzf1od  10640  expdivap  10824  fundm2domnop0  11080  swrdwrdsymbg  11211  ccatpfx  11248  swrdccat  11282  2shfti  11357  iooinsup  11803  isermulc2  11866  dvds2add  12351  dvds2sub  12352  dvdstr  12354  alzdvds  12380  divalg2  12452  lcmgcdlem  12614  lcmgcdeq  12620  isprm6  12684  pcqcl  12844  mgmplusf  13414  grpinva  13434  ismndd  13485  imasmnd2  13500  idmhm  13517  issubm2  13521  submid  13525  0mhm  13534  resmhm  13535  resmhm2  13536  resmhm2b  13537  mhmco  13538  mhmima  13539  gsumwsubmcl  13544  gsumwmhm  13546  grpinvcnv  13616  grpinvnzcl  13620  grpsubf  13627  imasgrp2  13662  qusgrp2  13665  mhmfmhm  13669  mulgnnsubcl  13686  mulgnn0z  13701  mulgnndir  13703  issubg4m  13745  isnsg3  13759  nsgid  13767  qusadd  13786  ghmmhm  13805  ghmmhmb  13806  idghm  13811  resghm  13812  ghmf1  13825  kerf1ghm  13826  qusghm  13834  ghmfghm  13878  invghm  13881  ablnsg  13886  srgfcl  13951  srgmulgass  13967  srglmhm  13971  srgrmhm  13972  ringlghm  14039  ringrghm  14040  opprringbg  14058  mulgass3  14063  isnzr2  14163  subrngringnsg  14184  issubrng2  14189  issubrg2  14220  domnmuln0  14252  islmodd  14272  lmodscaf  14289  lcomf  14306  rmodislmodlem  14329  issubrgd  14431  qusrhm  14507  qusmul2  14508  crngridl  14509  qusmulrng  14511  znidom  14636  psraddcl  14659  tgclb  14754  topbas  14756  neissex  14854  cnpnei  14908  txcnp  14960  psmetxrge0  15021  psmetlecl  15023  xmetlecl  15056  xmettpos  15059  elbl3ps  15083  elbl3  15084  metss  15183  comet  15188  bdxmet  15190  bdmet  15191  bl2ioo  15239  divcnap  15254  cncfcdm  15271  divccncfap  15279  dvrecap  15402  dvmptfsum  15414  cosz12  15469  gausslemma2dlem1a  15752  usgredg2vlem1  16035  usgredg2vlem2  16036