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 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3adant3r1  1243  3adant3r2  1244  3adant3r3  1245  3adant1l  1261  3adant1r  1262  mp3an1  1365  soinxp  4845  sotri  5183  fnfco  5564  mpoeq3dva  6152  fovcdmda  6233  ovelrn  6238  fnmpoovd  6451  nnmsucr  6761  fidifsnid  7173  exmidpw  7215  undiffi  7232  fidcenumlemim  7269  ltpopr  7963  ltexprlemdisj  7974  recexprlemdisj  7998  mul4  8460  add4  8489  2addsub  8542  addsubeq4  8543  subadd4  8572  muladd  8713  ltleadd  8776  divmulap  9008  divap0  9017  div23ap  9024  div12ap  9027  divsubdirap  9041  divcanap5  9047  divmuleqap  9050  divcanap6  9052  divdiv32ap  9053  div2subap  9170  letrp1  9181  lemul12b  9194  lediv1  9202  cju  9294  nndivre  9343  nndivtr  9349  nn0addge1  9614  nn0addge2  9615  peano2uz2  9758  uzind  9762  uzind3  9764  fzind  9766  fnn0ind  9767  uzind4  9998  qre  10035  irrmul  10058  rpdivcl  10091  rerpdivcl  10096  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  fzaddel  10476  fzrev  10502  frec2uzf1od  10858  expdivap  11042  fundm2domnop0  11316  swrdwrdsymbg  11452  ccatpfx  11489  swrdccat  11523  2shfti  11612  iooinsup  12062  isermulc2  12125  dvds2add  12611  dvds2sub  12612  dvdstr  12614  alzdvds  12640  divalg2  12712  lcmgcdlem  12874  lcmgcdeq  12880  isprm6  12945  pcqcl  13108  mgmplusf  13739  grpinva  13759  ismndd  13803  imasmnd2  13812  idmhm  13829  issubm2  13833  submid  13837  0mhm  13846  resmhm  13847  resmhm2  13848  resmhm2b  13849  mhmco  13850  mhmima  13851  gzsumwsubmcl  13854  gzsumwmhm  13856  grpinvcnv  13926  grpinvnzcl  13930  grpsubf  13937  imasgrp2  13966  qusgrp2  13969  mhmfmhm  13973  mulgnnsubcl  13990  mulgnn0z  14005  mulgnndir  14007  issubg4m  14049  isnsg3  14063  nsgid  14071  qusadd  14090  ghmmhm  14109  ghmmhmb  14110  idghm  14115  resghm  14116  ghmf1  14129  kerf1ghm  14130  qusghm  14138  ghmfghm  14214  invghm  14217  ablnsg  14222  srgfcl  14361  srgmulgass  14377  srglmhm  14381  srgrmhm  14382  ringlghm  14450  ringrghm  14451  opprringbg  14469  mulgass3  14475  isnzr2  14575  subrngringnsg  14597  issubrng2  14602  issubrg2  14633  domnmuln0  14666  islmodd  14713  lmodscaf  14731  lcomf  14748  rmodislmodlem  14771  issubrgd  14873  qusrhm  14949  qusmul2  14950  crngridl  14951  qusmulrng  14953  znidom  15076  asclghm  15109  asclrhm  15117  rnasclmulcl  15121  psraddcl  15156  tgclb  15257  topbas  15259  neissex  15357  cnpnei  15411  txcnp  15463  psmetxrge0  15524  psmetlecl  15526  xmetlecl  15559  xmettpos  15562  elbl3ps  15586  elbl3  15587  metss  15686  comet  15691  bdxmet  15693  bdmet  15694  bl2ioo  15742  divcnap  15757  cncfcdm  15774  divccncfap  15782  dvrecap  15905  dvmptfsum  15917  cosz12  15973  gausslemma2dlem1a  16343  usgredg2vlem1  16629  usgredg2vlem2  16630