Theorem 3expb 1230

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

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

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 1006

This theorem is referenced by:  3adant3r1  1238  3adant3r2  1239  3adant3r3  1240  3adant1l  1256  3adant1r  1257  mp3an1  1360  soinxp  4796  sotri  5132  fnfco  5511  mpoeq3dva  6085  fovcdmda  6166  ovelrn  6171  fnmpoovd  6380  nnmsucr  6656  fidifsnid  7058  exmidpw  7100  undiffi  7117  fidcenumlemim  7151  ltpopr  7815  ltexprlemdisj  7826  recexprlemdisj  7850  mul4  8311  add4  8340  2addsub  8393  addsubeq4  8394  subadd4  8423  muladd  8563  ltleadd  8626  divmulap  8855  divap0  8864  div23ap  8871  div12ap  8874  divsubdirap  8888  divcanap5  8894  divmuleqap  8897  divcanap6  8899  divdiv32ap  8900  div2subap  9017  letrp1  9028  lemul12b  9041  lediv1  9049  cju  9141  nndivre  9179  nndivtr  9185  nn0addge1  9448  nn0addge2  9449  peano2uz2  9587  uzind  9591  uzind3  9593  fzind  9595  fnn0ind  9596  uzind4  9822  qre  9859  irrmul  9881  rpdivcl  9914  rerpdivcl  9919  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  fzaddel  10294  fzrev  10319  frec2uzf1od  10669  expdivap  10853  fundm2domnop0  11113  swrdwrdsymbg  11249  ccatpfx  11286  swrdccat  11320  2shfti  11396  iooinsup  11842  isermulc2  11905  dvds2add  12391  dvds2sub  12392  dvdstr  12394  alzdvds  12420  divalg2  12492  lcmgcdlem  12654  lcmgcdeq  12660  isprm6  12724  pcqcl  12884  mgmplusf  13454  grpinva  13474  ismndd  13525  imasmnd2  13540  idmhm  13557  issubm2  13561  submid  13565  0mhm  13574  resmhm  13575  resmhm2  13576  resmhm2b  13577  mhmco  13578  mhmima  13579  gsumwsubmcl  13584  gsumwmhm  13586  grpinvcnv  13656  grpinvnzcl  13660  grpsubf  13667  imasgrp2  13702  qusgrp2  13705  mhmfmhm  13709  mulgnnsubcl  13726  mulgnn0z  13741  mulgnndir  13743  issubg4m  13785  isnsg3  13799  nsgid  13807  qusadd  13826  ghmmhm  13845  ghmmhmb  13846  idghm  13851  resghm  13852  ghmf1  13865  kerf1ghm  13866  qusghm  13874  ghmfghm  13918  invghm  13921  ablnsg  13926  srgfcl  13992  srgmulgass  14008  srglmhm  14012  srgrmhm  14013  ringlghm  14080  ringrghm  14081  opprringbg  14099  mulgass3  14104  isnzr2  14204  subrngringnsg  14225  issubrng2  14230  issubrg2  14261  domnmuln0  14293  islmodd  14313  lmodscaf  14330  lcomf  14347  rmodislmodlem  14370  issubrgd  14472  qusrhm  14548  qusmul2  14549  crngridl  14550  qusmulrng  14552  znidom  14677  psraddcl  14700  tgclb  14795  topbas  14797  neissex  14895  cnpnei  14949  txcnp  15001  psmetxrge0  15062  psmetlecl  15064  xmetlecl  15097  xmettpos  15100  elbl3ps  15124  elbl3  15125  metss  15224  comet  15229  bdxmet  15231  bdmet  15232  bl2ioo  15280  divcnap  15295  cncfcdm  15312  divccncfap  15320  dvrecap  15443  dvmptfsum  15455  cosz12  15510  gausslemma2dlem1a  15793  usgredg2vlem1  16079  usgredg2vlem2  16080