Theorem 3expb 1207

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

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

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 983

This theorem is referenced by:  3adant3r1  1215  3adant3r2  1216  3adant3r3  1217  3adant1l  1233  3adant1r  1234  mp3an1  1337  soinxp  4745  sotri  5078  fnfco  5450  mpoeq3dva  6009  fovcdmda  6090  ovelrn  6095  fnmpoovd  6301  nnmsucr  6574  fidifsnid  6968  exmidpw  7005  undiffi  7022  fidcenumlemim  7054  ltpopr  7708  ltexprlemdisj  7719  recexprlemdisj  7743  mul4  8204  add4  8233  2addsub  8286  addsubeq4  8287  subadd4  8316  muladd  8456  ltleadd  8519  divmulap  8748  divap0  8757  div23ap  8764  div12ap  8767  divsubdirap  8781  divcanap5  8787  divmuleqap  8790  divcanap6  8792  divdiv32ap  8793  div2subap  8910  letrp1  8921  lemul12b  8934  lediv1  8942  cju  9034  nndivre  9072  nndivtr  9078  nn0addge1  9341  nn0addge2  9342  peano2uz2  9480  uzind  9484  uzind3  9486  fzind  9488  fnn0ind  9489  uzind4  9709  qre  9746  irrmul  9768  rpdivcl  9801  rerpdivcl  9806  iccshftr  10116  iccshftl  10118  iccdil  10120  icccntr  10122  fzaddel  10181  fzrev  10206  frec2uzf1od  10551  expdivap  10735  fundm2domnop0  10990  swrdwrdsymbg  11117  2shfti  11142  iooinsup  11588  isermulc2  11651  dvds2add  12136  dvds2sub  12137  dvdstr  12139  alzdvds  12165  divalg2  12237  lcmgcdlem  12399  lcmgcdeq  12405  isprm6  12469  pcqcl  12629  mgmplusf  13198  grpinva  13218  ismndd  13269  imasmnd2  13284  idmhm  13301  issubm2  13305  submid  13309  0mhm  13318  resmhm  13319  resmhm2  13320  resmhm2b  13321  mhmco  13322  mhmima  13323  gsumwsubmcl  13328  gsumwmhm  13330  grpinvcnv  13400  grpinvnzcl  13404  grpsubf  13411  imasgrp2  13446  qusgrp2  13449  mhmfmhm  13453  mulgnnsubcl  13470  mulgnn0z  13485  mulgnndir  13487  issubg4m  13529  isnsg3  13543  nsgid  13551  qusadd  13570  ghmmhm  13589  ghmmhmb  13590  idghm  13595  resghm  13596  ghmf1  13609  kerf1ghm  13610  qusghm  13618  ghmfghm  13662  invghm  13665  ablnsg  13670  srgfcl  13735  srgmulgass  13751  srglmhm  13755  srgrmhm  13756  ringlghm  13823  ringrghm  13824  opprringbg  13842  mulgass3  13847  isnzr2  13946  subrngringnsg  13967  issubrng2  13972  issubrg2  14003  domnmuln0  14035  islmodd  14055  lmodscaf  14072  lcomf  14089  rmodislmodlem  14112  issubrgd  14214  qusrhm  14290  qusmul2  14291  crngridl  14292  qusmulrng  14294  znidom  14419  psraddcl  14442  tgclb  14537  topbas  14539  neissex  14637  cnpnei  14691  txcnp  14743  psmetxrge0  14804  psmetlecl  14806  xmetlecl  14839  xmettpos  14842  elbl3ps  14866  elbl3  14867  metss  14966  comet  14971  bdxmet  14973  bdmet  14974  bl2ioo  15022  divcnap  15037  cncfcdm  15054  divccncfap  15062  dvrecap  15185  dvmptfsum  15197  cosz12  15252  gausslemma2dlem1a  15535