Theorem 3expb 1231

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

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

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 1007

This theorem is referenced by:  3adant3r1  1239  3adant3r2  1240  3adant3r3  1241  3adant1l  1257  3adant1r  1258  mp3an1  1361  soinxp  4802  sotri  5139  fnfco  5519  mpoeq3dva  6095  fovcdmda  6176  ovelrn  6181  fnmpoovd  6389  nnmsucr  6699  fidifsnid  7101  exmidpw  7143  undiffi  7160  fidcenumlemim  7194  ltpopr  7858  ltexprlemdisj  7869  recexprlemdisj  7893  mul4  8353  add4  8382  2addsub  8435  addsubeq4  8436  subadd4  8465  muladd  8605  ltleadd  8668  divmulap  8897  divap0  8906  div23ap  8913  div12ap  8916  divsubdirap  8930  divcanap5  8936  divmuleqap  8939  divcanap6  8941  divdiv32ap  8942  div2subap  9059  letrp1  9070  lemul12b  9083  lediv1  9091  cju  9183  nndivre  9221  nndivtr  9227  nn0addge1  9490  nn0addge2  9491  peano2uz2  9631  uzind  9635  uzind3  9637  fzind  9639  fnn0ind  9640  uzind4  9866  qre  9903  irrmul  9925  rpdivcl  9958  rerpdivcl  9963  iccshftr  10273  iccshftl  10275  iccdil  10277  icccntr  10279  fzaddel  10339  fzrev  10364  frec2uzf1od  10714  expdivap  10898  fundm2domnop0  11158  swrdwrdsymbg  11294  ccatpfx  11331  swrdccat  11365  2shfti  11454  iooinsup  11900  isermulc2  11963  dvds2add  12449  dvds2sub  12450  dvdstr  12452  alzdvds  12478  divalg2  12550  lcmgcdlem  12712  lcmgcdeq  12718  isprm6  12782  pcqcl  12942  mgmplusf  13512  grpinva  13532  ismndd  13583  imasmnd2  13598  idmhm  13615  issubm2  13619  submid  13623  0mhm  13632  resmhm  13633  resmhm2  13634  resmhm2b  13635  mhmco  13636  mhmima  13637  gsumwsubmcl  13642  gsumwmhm  13644  grpinvcnv  13714  grpinvnzcl  13718  grpsubf  13725  imasgrp2  13760  qusgrp2  13763  mhmfmhm  13767  mulgnnsubcl  13784  mulgnn0z  13799  mulgnndir  13801  issubg4m  13843  isnsg3  13857  nsgid  13865  qusadd  13884  ghmmhm  13903  ghmmhmb  13904  idghm  13909  resghm  13910  ghmf1  13923  kerf1ghm  13924  qusghm  13932  ghmfghm  13976  invghm  13979  ablnsg  13984  srgfcl  14050  srgmulgass  14066  srglmhm  14070  srgrmhm  14071  ringlghm  14138  ringrghm  14139  opprringbg  14157  mulgass3  14162  isnzr2  14262  subrngringnsg  14283  issubrng2  14288  issubrg2  14319  domnmuln0  14352  islmodd  14372  lmodscaf  14389  lcomf  14406  rmodislmodlem  14429  issubrgd  14531  qusrhm  14607  qusmul2  14608  crngridl  14609  qusmulrng  14611  znidom  14736  psraddcl  14764  tgclb  14859  topbas  14861  neissex  14959  cnpnei  15013  txcnp  15065  psmetxrge0  15126  psmetlecl  15128  xmetlecl  15161  xmettpos  15164  elbl3ps  15188  elbl3  15189  metss  15288  comet  15293  bdxmet  15295  bdmet  15296  bl2ioo  15344  divcnap  15359  cncfcdm  15376  divccncfap  15384  dvrecap  15507  dvmptfsum  15519  cosz12  15574  gausslemma2dlem1a  15860  usgredg2vlem1  16146  usgredg2vlem2  16147