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  4820  sotri  5158  fnfco  5539  mpoeq3dva  6117  fovcdmda  6198  ovelrn  6203  fnmpoovd  6411  nnmsucr  6721  fidifsnid  7126  exmidpw  7168  undiffi  7185  fidcenumlemim  7222  ltpopr  7910  ltexprlemdisj  7921  recexprlemdisj  7945  mul4  8405  add4  8434  2addsub  8487  addsubeq4  8488  subadd4  8517  muladd  8657  ltleadd  8720  divmulap  8949  divap0  8958  div23ap  8965  div12ap  8968  divsubdirap  8982  divcanap5  8988  divmuleqap  8991  divcanap6  8993  divdiv32ap  8994  div2subap  9111  letrp1  9122  lemul12b  9135  lediv1  9143  cju  9235  nndivre  9273  nndivtr  9279  nn0addge1  9542  nn0addge2  9543  peano2uz2  9685  uzind  9689  uzind3  9691  fzind  9693  fnn0ind  9694  uzind4  9920  qre  9957  irrmul  9979  rpdivcl  10012  rerpdivcl  10017  iccshftr  10327  iccshftl  10329  iccdil  10331  icccntr  10333  fzaddel  10393  fzrev  10418  frec2uzf1od  10768  expdivap  10952  fundm2domnop0  11220  swrdwrdsymbg  11356  ccatpfx  11393  swrdccat  11427  2shfti  11516  iooinsup  11962  isermulc2  12025  dvds2add  12511  dvds2sub  12512  dvdstr  12514  alzdvds  12540  divalg2  12612  lcmgcdlem  12774  lcmgcdeq  12780  isprm6  12844  pcqcl  13004  mgmplusf  13579  grpinva  13599  ismndd  13650  imasmnd2  13665  idmhm  13682  issubm2  13686  submid  13690  0mhm  13699  resmhm  13700  resmhm2  13701  resmhm2b  13702  mhmco  13703  mhmima  13704  gsumwsubmcl  13709  gsumwmhm  13711  grpinvcnv  13781  grpinvnzcl  13785  grpsubf  13792  imasgrp2  13827  qusgrp2  13830  mhmfmhm  13834  mulgnnsubcl  13851  mulgnn0z  13866  mulgnndir  13868  issubg4m  13910  isnsg3  13924  nsgid  13932  qusadd  13951  ghmmhm  13970  ghmmhmb  13971  idghm  13976  resghm  13977  ghmf1  13990  kerf1ghm  13991  qusghm  13999  ghmfghm  14043  invghm  14046  ablnsg  14051  srgfcl  14117  srgmulgass  14133  srglmhm  14137  srgrmhm  14138  ringlghm  14205  ringrghm  14206  opprringbg  14224  mulgass3  14229  isnzr2  14329  subrngringnsg  14350  issubrng2  14355  issubrg2  14386  domnmuln0  14419  islmodd  14441  lmodscaf  14458  lcomf  14475  rmodislmodlem  14498  issubrgd  14600  qusrhm  14676  qusmul2  14677  crngridl  14678  qusmulrng  14680  znidom  14805  psraddcl  14835  tgclb  14930  topbas  14932  neissex  15030  cnpnei  15084  txcnp  15136  psmetxrge0  15197  psmetlecl  15199  xmetlecl  15232  xmettpos  15235  elbl3ps  15259  elbl3  15260  metss  15359  comet  15364  bdxmet  15366  bdmet  15367  bl2ioo  15415  divcnap  15430  cncfcdm  15447  divccncfap  15455  dvrecap  15578  dvmptfsum  15590  cosz12  15645  gausslemma2dlem1a  15931  usgredg2vlem1  16217  usgredg2vlem2  16218