Theorem 3expb 1235

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

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

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 1011

This theorem is referenced by:  3adant3r1  1243  3adant3r2  1244  3adant3r3  1245  3adant1l  1261  3adant1r  1262  mp3an1  1365  soinxp  4840  sotri  5178  fnfco  5559  mpoeq3dva  6142  fovcdmda  6223  ovelrn  6228  fnmpoovd  6441  nnmsucr  6751  fidifsnid  7163  exmidpw  7205  undiffi  7222  fidcenumlemim  7259  ltpopr  7952  ltexprlemdisj  7963  recexprlemdisj  7987  mul4  8448  add4  8477  2addsub  8530  addsubeq4  8531  subadd4  8560  muladd  8701  ltleadd  8764  divmulap  8995  divap0  9004  div23ap  9011  div12ap  9014  divsubdirap  9028  divcanap5  9034  divmuleqap  9037  divcanap6  9039  divdiv32ap  9040  div2subap  9157  letrp1  9168  lemul12b  9181  lediv1  9189  cju  9281  nndivre  9319  nndivtr  9325  nn0addge1  9588  nn0addge2  9589  peano2uz2  9732  uzind  9736  uzind3  9738  fzind  9740  fnn0ind  9741  uzind4  9967  qre  10004  irrmul  10026  rpdivcl  10059  rerpdivcl  10064  iccshftr  10375  iccshftl  10377  iccdil  10379  icccntr  10381  fzaddel  10443  fzrev  10469  frec2uzf1od  10821  expdivap  11005  fundm2domnop0  11278  swrdwrdsymbg  11414  ccatpfx  11451  swrdccat  11485  2shfti  11574  iooinsup  12021  isermulc2  12084  dvds2add  12570  dvds2sub  12571  dvdstr  12573  alzdvds  12599  divalg2  12671  lcmgcdlem  12833  lcmgcdeq  12839  isprm6  12903  pcqcl  13063  mgmplusf  13663  grpinva  13683  ismndd  13727  imasmnd2  13736  idmhm  13753  issubm2  13757  submid  13761  0mhm  13770  resmhm  13771  resmhm2  13772  resmhm2b  13773  mhmco  13774  mhmima  13775  gzsumwsubmcl  13778  gzsumwmhm  13780  grpinvcnv  13850  grpinvnzcl  13854  grpsubf  13861  imasgrp2  13890  qusgrp2  13893  mhmfmhm  13897  mulgnnsubcl  13914  mulgnn0z  13929  mulgnndir  13931  issubg4m  13973  isnsg3  13987  nsgid  13995  qusadd  14014  ghmmhm  14033  ghmmhmb  14034  idghm  14039  resghm  14040  ghmf1  14053  kerf1ghm  14054  qusghm  14062  ghmfghm  14107  invghm  14110  ablnsg  14115  srgfcl  14251  srgmulgass  14267  srglmhm  14271  srgrmhm  14272  ringlghm  14339  ringrghm  14340  opprringbg  14358  mulgass3  14364  isnzr2  14464  subrngringnsg  14486  issubrng2  14491  issubrg2  14522  domnmuln0  14555  islmodd  14602  lmodscaf  14619  lcomf  14636  rmodislmodlem  14659  issubrgd  14761  qusrhm  14837  qusmul2  14838  crngridl  14839  qusmulrng  14841  znidom  14964  psraddcl  14994  tgclb  15089  topbas  15091  neissex  15189  cnpnei  15243  txcnp  15295  psmetxrge0  15356  psmetlecl  15358  xmetlecl  15391  xmettpos  15394  elbl3ps  15418  elbl3  15419  metss  15518  comet  15523  bdxmet  15525  bdmet  15526  bl2ioo  15574  divcnap  15589  cncfcdm  15606  divccncfap  15614  dvrecap  15737  dvmptfsum  15749  cosz12  15804  gausslemma2dlem1a  16091  usgredg2vlem1  16377  usgredg2vlem2  16378