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  6084  fovcdmda  6165  ovelrn  6170  fnmpoovd  6379  nnmsucr  6655  fidifsnid  7057  exmidpw  7099  undiffi  7116  fidcenumlemim  7150  ltpopr  7814  ltexprlemdisj  7825  recexprlemdisj  7849  mul4  8310  add4  8339  2addsub  8392  addsubeq4  8393  subadd4  8422  muladd  8562  ltleadd  8625  divmulap  8854  divap0  8863  div23ap  8870  div12ap  8873  divsubdirap  8887  divcanap5  8893  divmuleqap  8896  divcanap6  8898  divdiv32ap  8899  div2subap  9016  letrp1  9027  lemul12b  9040  lediv1  9048  cju  9140  nndivre  9178  nndivtr  9184  nn0addge1  9447  nn0addge2  9448  peano2uz2  9586  uzind  9590  uzind3  9592  fzind  9594  fnn0ind  9595  uzind4  9821  qre  9858  irrmul  9880  rpdivcl  9913  rerpdivcl  9918  iccshftr  10228  iccshftl  10230  iccdil  10232  icccntr  10234  fzaddel  10293  fzrev  10318  frec2uzf1od  10667  expdivap  10851  fundm2domnop0  11108  swrdwrdsymbg  11244  ccatpfx  11281  swrdccat  11315  2shfti  11391  iooinsup  11837  isermulc2  11900  dvds2add  12385  dvds2sub  12386  dvdstr  12388  alzdvds  12414  divalg2  12486  lcmgcdlem  12648  lcmgcdeq  12654  isprm6  12718  pcqcl  12878  mgmplusf  13448  grpinva  13468  ismndd  13519  imasmnd2  13534  idmhm  13551  issubm2  13555  submid  13559  0mhm  13568  resmhm  13569  resmhm2  13570  resmhm2b  13571  mhmco  13572  mhmima  13573  gsumwsubmcl  13578  gsumwmhm  13580  grpinvcnv  13650  grpinvnzcl  13654  grpsubf  13661  imasgrp2  13696  qusgrp2  13699  mhmfmhm  13703  mulgnnsubcl  13720  mulgnn0z  13735  mulgnndir  13737  issubg4m  13779  isnsg3  13793  nsgid  13801  qusadd  13820  ghmmhm  13839  ghmmhmb  13840  idghm  13845  resghm  13846  ghmf1  13859  kerf1ghm  13860  qusghm  13868  ghmfghm  13912  invghm  13915  ablnsg  13920  srgfcl  13985  srgmulgass  14001  srglmhm  14005  srgrmhm  14006  ringlghm  14073  ringrghm  14074  opprringbg  14092  mulgass3  14097  isnzr2  14197  subrngringnsg  14218  issubrng2  14223  issubrg2  14254  domnmuln0  14286  islmodd  14306  lmodscaf  14323  lcomf  14340  rmodislmodlem  14363  issubrgd  14465  qusrhm  14541  qusmul2  14542  crngridl  14543  qusmulrng  14545  znidom  14670  psraddcl  14693  tgclb  14788  topbas  14790  neissex  14888  cnpnei  14942  txcnp  14994  psmetxrge0  15055  psmetlecl  15057  xmetlecl  15090  xmettpos  15093  elbl3ps  15117  elbl3  15118  metss  15217  comet  15222  bdxmet  15224  bdmet  15225  bl2ioo  15273  divcnap  15288  cncfcdm  15305  divccncfap  15313  dvrecap  15436  dvmptfsum  15448  cosz12  15503  gausslemma2dlem1a  15786  usgredg2vlem1  16072  usgredg2vlem2  16073