Theorem 3expb 1206

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

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

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 982

This theorem is referenced by:  3adant3r1  1214  3adant3r2  1215  3adant3r3  1216  3adant1l  1232  3adant1r  1233  mp3an1  1336  soinxp  4744  sotri  5077  fnfco  5449  mpoeq3dva  6008  fovcdmda  6089  ovelrn  6094  fnmpoovd  6300  nnmsucr  6573  fidifsnid  6967  exmidpw  7004  undiffi  7021  fidcenumlemim  7053  ltpopr  7707  ltexprlemdisj  7718  recexprlemdisj  7742  mul4  8203  add4  8232  2addsub  8285  addsubeq4  8286  subadd4  8315  muladd  8455  ltleadd  8518  divmulap  8747  divap0  8756  div23ap  8763  div12ap  8766  divsubdirap  8780  divcanap5  8786  divmuleqap  8789  divcanap6  8791  divdiv32ap  8792  div2subap  8909  letrp1  8920  lemul12b  8933  lediv1  8941  cju  9033  nndivre  9071  nndivtr  9077  nn0addge1  9340  nn0addge2  9341  peano2uz2  9479  uzind  9483  uzind3  9485  fzind  9487  fnn0ind  9488  uzind4  9708  qre  9745  irrmul  9767  rpdivcl  9800  rerpdivcl  9805  iccshftr  10115  iccshftl  10117  iccdil  10119  icccntr  10121  fzaddel  10180  fzrev  10205  frec2uzf1od  10549  expdivap  10733  fundm2domnop0  10988  2shfti  11113  iooinsup  11559  isermulc2  11622  dvds2add  12107  dvds2sub  12108  dvdstr  12110  alzdvds  12136  divalg2  12208  lcmgcdlem  12370  lcmgcdeq  12376  isprm6  12440  pcqcl  12600  mgmplusf  13169  grpinva  13189  ismndd  13240  imasmnd2  13255  idmhm  13272  issubm2  13276  submid  13280  0mhm  13289  resmhm  13290  resmhm2  13291  resmhm2b  13292  mhmco  13293  mhmima  13294  gsumwsubmcl  13299  gsumwmhm  13301  grpinvcnv  13371  grpinvnzcl  13375  grpsubf  13382  imasgrp2  13417  qusgrp2  13420  mhmfmhm  13424  mulgnnsubcl  13441  mulgnn0z  13456  mulgnndir  13458  issubg4m  13500  isnsg3  13514  nsgid  13522  qusadd  13541  ghmmhm  13560  ghmmhmb  13561  idghm  13566  resghm  13567  ghmf1  13580  kerf1ghm  13581  qusghm  13589  ghmfghm  13633  invghm  13636  ablnsg  13641  srgfcl  13706  srgmulgass  13722  srglmhm  13726  srgrmhm  13727  ringlghm  13794  ringrghm  13795  opprringbg  13813  mulgass3  13818  isnzr2  13917  subrngringnsg  13938  issubrng2  13943  issubrg2  13974  domnmuln0  14006  islmodd  14026  lmodscaf  14043  lcomf  14060  rmodislmodlem  14083  issubrgd  14185  qusrhm  14261  qusmul2  14262  crngridl  14263  qusmulrng  14265  znidom  14390  psraddcl  14413  tgclb  14508  topbas  14510  neissex  14608  cnpnei  14662  txcnp  14714  psmetxrge0  14775  psmetlecl  14777  xmetlecl  14810  xmettpos  14813  elbl3ps  14837  elbl3  14838  metss  14937  comet  14942  bdxmet  14944  bdmet  14945  bl2ioo  14993  divcnap  15008  cncfcdm  15025  divccncfap  15033  dvrecap  15156  dvmptfsum  15168  cosz12  15223  gausslemma2dlem1a  15506