Theorem 3expb 1228

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

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

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 1004

This theorem is referenced by:  3adant3r1  1236  3adant3r2  1237  3adant3r3  1238  3adant1l  1254  3adant1r  1255  mp3an1  1358  soinxp  4788  sotri  5123  fnfco  5499  mpoeq3dva  6067  fovcdmda  6148  ovelrn  6153  fnmpoovd  6359  nnmsucr  6632  fidifsnid  7029  exmidpw  7066  undiffi  7083  fidcenumlemim  7115  ltpopr  7778  ltexprlemdisj  7789  recexprlemdisj  7813  mul4  8274  add4  8303  2addsub  8356  addsubeq4  8357  subadd4  8386  muladd  8526  ltleadd  8589  divmulap  8818  divap0  8827  div23ap  8834  div12ap  8837  divsubdirap  8851  divcanap5  8857  divmuleqap  8860  divcanap6  8862  divdiv32ap  8863  div2subap  8980  letrp1  8991  lemul12b  9004  lediv1  9012  cju  9104  nndivre  9142  nndivtr  9148  nn0addge1  9411  nn0addge2  9412  peano2uz2  9550  uzind  9554  uzind3  9556  fzind  9558  fnn0ind  9559  uzind4  9779  qre  9816  irrmul  9838  rpdivcl  9871  rerpdivcl  9876  iccshftr  10186  iccshftl  10188  iccdil  10190  icccntr  10192  fzaddel  10251  fzrev  10276  frec2uzf1od  10623  expdivap  10807  fundm2domnop0  11062  swrdwrdsymbg  11191  ccatpfx  11228  swrdccat  11262  2shfti  11337  iooinsup  11783  isermulc2  11846  dvds2add  12331  dvds2sub  12332  dvdstr  12334  alzdvds  12360  divalg2  12432  lcmgcdlem  12594  lcmgcdeq  12600  isprm6  12664  pcqcl  12824  mgmplusf  13394  grpinva  13414  ismndd  13465  imasmnd2  13480  idmhm  13497  issubm2  13501  submid  13505  0mhm  13514  resmhm  13515  resmhm2  13516  resmhm2b  13517  mhmco  13518  mhmima  13519  gsumwsubmcl  13524  gsumwmhm  13526  grpinvcnv  13596  grpinvnzcl  13600  grpsubf  13607  imasgrp2  13642  qusgrp2  13645  mhmfmhm  13649  mulgnnsubcl  13666  mulgnn0z  13681  mulgnndir  13683  issubg4m  13725  isnsg3  13739  nsgid  13747  qusadd  13766  ghmmhm  13785  ghmmhmb  13786  idghm  13791  resghm  13792  ghmf1  13805  kerf1ghm  13806  qusghm  13814  ghmfghm  13858  invghm  13861  ablnsg  13866  srgfcl  13931  srgmulgass  13947  srglmhm  13951  srgrmhm  13952  ringlghm  14019  ringrghm  14020  opprringbg  14038  mulgass3  14043  isnzr2  14142  subrngringnsg  14163  issubrng2  14168  issubrg2  14199  domnmuln0  14231  islmodd  14251  lmodscaf  14268  lcomf  14285  rmodislmodlem  14308  issubrgd  14410  qusrhm  14486  qusmul2  14487  crngridl  14488  qusmulrng  14490  znidom  14615  psraddcl  14638  tgclb  14733  topbas  14735  neissex  14833  cnpnei  14887  txcnp  14939  psmetxrge0  15000  psmetlecl  15002  xmetlecl  15035  xmettpos  15038  elbl3ps  15062  elbl3  15063  metss  15162  comet  15167  bdxmet  15169  bdmet  15170  bl2ioo  15218  divcnap  15233  cncfcdm  15250  divccncfap  15258  dvrecap  15381  dvmptfsum  15393  cosz12  15448  gausslemma2dlem1a  15731  usgredg2vlem1  16014  usgredg2vlem2  16015