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  1335  soinxp  4734  sotri  5066  fnfco  5435  mpoeq3dva  5990  fovcdmda  6071  ovelrn  6076  fnmpoovd  6282  nnmsucr  6555  fidifsnid  6941  exmidpw  6978  undiffi  6995  fidcenumlemim  7027  ltpopr  7681  ltexprlemdisj  7692  recexprlemdisj  7716  mul4  8177  add4  8206  2addsub  8259  addsubeq4  8260  subadd4  8289  muladd  8429  ltleadd  8492  divmulap  8721  divap0  8730  div23ap  8737  div12ap  8740  divsubdirap  8754  divcanap5  8760  divmuleqap  8763  divcanap6  8765  divdiv32ap  8766  div2subap  8883  letrp1  8894  lemul12b  8907  lediv1  8915  cju  9007  nndivre  9045  nndivtr  9051  nn0addge1  9314  nn0addge2  9315  peano2uz2  9452  uzind  9456  uzind3  9458  fzind  9460  fnn0ind  9461  uzind4  9681  qre  9718  irrmul  9740  rpdivcl  9773  rerpdivcl  9778  iccshftr  10088  iccshftl  10090  iccdil  10092  icccntr  10094  fzaddel  10153  fzrev  10178  frec2uzf1od  10517  expdivap  10701  2shfti  11015  iooinsup  11461  isermulc2  11524  dvds2add  12009  dvds2sub  12010  dvdstr  12012  alzdvds  12038  divalg2  12110  lcmgcdlem  12272  lcmgcdeq  12278  isprm6  12342  pcqcl  12502  mgmplusf  13070  grpinva  13090  ismndd  13141  imasmnd2  13156  idmhm  13173  issubm2  13177  submid  13181  0mhm  13190  resmhm  13191  resmhm2  13192  resmhm2b  13193  mhmco  13194  mhmima  13195  gsumwsubmcl  13200  gsumwmhm  13202  grpinvcnv  13272  grpinvnzcl  13276  grpsubf  13283  imasgrp2  13318  qusgrp2  13321  mhmfmhm  13325  mulgnnsubcl  13342  mulgnn0z  13357  mulgnndir  13359  issubg4m  13401  isnsg3  13415  nsgid  13423  qusadd  13442  ghmmhm  13461  ghmmhmb  13462  idghm  13467  resghm  13468  ghmf1  13481  kerf1ghm  13482  qusghm  13490  ghmfghm  13534  invghm  13537  ablnsg  13542  srgfcl  13607  srgmulgass  13623  srglmhm  13627  srgrmhm  13628  ringlghm  13695  ringrghm  13696  opprringbg  13714  mulgass3  13719  isnzr2  13818  subrngringnsg  13839  issubrng2  13844  issubrg2  13875  domnmuln0  13907  islmodd  13927  lmodscaf  13944  lcomf  13961  rmodislmodlem  13984  issubrgd  14086  qusrhm  14162  qusmul2  14163  crngridl  14164  qusmulrng  14166  znidom  14291  psraddcl  14314  tgclb  14409  topbas  14411  neissex  14509  cnpnei  14563  txcnp  14615  psmetxrge0  14676  psmetlecl  14678  xmetlecl  14711  xmettpos  14714  elbl3ps  14738  elbl3  14739  metss  14838  comet  14843  bdxmet  14845  bdmet  14846  bl2ioo  14894  divcnap  14909  cncfcdm  14926  divccncfap  14934  dvrecap  15057  dvmptfsum  15069  cosz12  15124  gausslemma2dlem1a  15407