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  4794  sotri  5130  fnfco  5508  mpoeq3dva  6080  fovcdmda  6161  ovelrn  6166  fnmpoovd  6375  nnmsucr  6651  fidifsnid  7053  exmidpw  7093  undiffi  7110  fidcenumlemim  7142  ltpopr  7805  ltexprlemdisj  7816  recexprlemdisj  7840  mul4  8301  add4  8330  2addsub  8383  addsubeq4  8384  subadd4  8413  muladd  8553  ltleadd  8616  divmulap  8845  divap0  8854  div23ap  8861  div12ap  8864  divsubdirap  8878  divcanap5  8884  divmuleqap  8887  divcanap6  8889  divdiv32ap  8890  div2subap  9007  letrp1  9018  lemul12b  9031  lediv1  9039  cju  9131  nndivre  9169  nndivtr  9175  nn0addge1  9438  nn0addge2  9439  peano2uz2  9577  uzind  9581  uzind3  9583  fzind  9585  fnn0ind  9586  uzind4  9812  qre  9849  irrmul  9871  rpdivcl  9904  rerpdivcl  9909  iccshftr  10219  iccshftl  10221  iccdil  10223  icccntr  10225  fzaddel  10284  fzrev  10309  frec2uzf1od  10658  expdivap  10842  fundm2domnop0  11099  swrdwrdsymbg  11235  ccatpfx  11272  swrdccat  11306  2shfti  11382  iooinsup  11828  isermulc2  11891  dvds2add  12376  dvds2sub  12377  dvdstr  12379  alzdvds  12405  divalg2  12477  lcmgcdlem  12639  lcmgcdeq  12645  isprm6  12709  pcqcl  12869  mgmplusf  13439  grpinva  13459  ismndd  13510  imasmnd2  13525  idmhm  13542  issubm2  13546  submid  13550  0mhm  13559  resmhm  13560  resmhm2  13561  resmhm2b  13562  mhmco  13563  mhmima  13564  gsumwsubmcl  13569  gsumwmhm  13571  grpinvcnv  13641  grpinvnzcl  13645  grpsubf  13652  imasgrp2  13687  qusgrp2  13690  mhmfmhm  13694  mulgnnsubcl  13711  mulgnn0z  13726  mulgnndir  13728  issubg4m  13770  isnsg3  13784  nsgid  13792  qusadd  13811  ghmmhm  13830  ghmmhmb  13831  idghm  13836  resghm  13837  ghmf1  13850  kerf1ghm  13851  qusghm  13859  ghmfghm  13903  invghm  13906  ablnsg  13911  srgfcl  13976  srgmulgass  13992  srglmhm  13996  srgrmhm  13997  ringlghm  14064  ringrghm  14065  opprringbg  14083  mulgass3  14088  isnzr2  14188  subrngringnsg  14209  issubrng2  14214  issubrg2  14245  domnmuln0  14277  islmodd  14297  lmodscaf  14314  lcomf  14331  rmodislmodlem  14354  issubrgd  14456  qusrhm  14532  qusmul2  14533  crngridl  14534  qusmulrng  14536  znidom  14661  psraddcl  14684  tgclb  14779  topbas  14781  neissex  14879  cnpnei  14933  txcnp  14985  psmetxrge0  15046  psmetlecl  15048  xmetlecl  15081  xmettpos  15084  elbl3ps  15108  elbl3  15109  metss  15208  comet  15213  bdxmet  15215  bdmet  15216  bl2ioo  15264  divcnap  15279  cncfcdm  15296  divccncfap  15304  dvrecap  15427  dvmptfsum  15439  cosz12  15494  gausslemma2dlem1a  15777  usgredg2vlem1  16061  usgredg2vlem2  16062