Theorem 3expb 1207

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

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

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 983

This theorem is referenced by:  3adant3r1  1215  3adant3r2  1216  3adant3r3  1217  3adant1l  1233  3adant1r  1234  mp3an1  1337  soinxp  4763  sotri  5097  fnfco  5472  mpoeq3dva  6032  fovcdmda  6113  ovelrn  6118  fnmpoovd  6324  nnmsucr  6597  fidifsnid  6994  exmidpw  7031  undiffi  7048  fidcenumlemim  7080  ltpopr  7743  ltexprlemdisj  7754  recexprlemdisj  7778  mul4  8239  add4  8268  2addsub  8321  addsubeq4  8322  subadd4  8351  muladd  8491  ltleadd  8554  divmulap  8783  divap0  8792  div23ap  8799  div12ap  8802  divsubdirap  8816  divcanap5  8822  divmuleqap  8825  divcanap6  8827  divdiv32ap  8828  div2subap  8945  letrp1  8956  lemul12b  8969  lediv1  8977  cju  9069  nndivre  9107  nndivtr  9113  nn0addge1  9376  nn0addge2  9377  peano2uz2  9515  uzind  9519  uzind3  9521  fzind  9523  fnn0ind  9524  uzind4  9744  qre  9781  irrmul  9803  rpdivcl  9836  rerpdivcl  9841  iccshftr  10151  iccshftl  10153  iccdil  10155  icccntr  10157  fzaddel  10216  fzrev  10241  frec2uzf1od  10588  expdivap  10772  fundm2domnop0  11027  swrdwrdsymbg  11155  ccatpfx  11192  swrdccat  11226  2shfti  11257  iooinsup  11703  isermulc2  11766  dvds2add  12251  dvds2sub  12252  dvdstr  12254  alzdvds  12280  divalg2  12352  lcmgcdlem  12514  lcmgcdeq  12520  isprm6  12584  pcqcl  12744  mgmplusf  13313  grpinva  13333  ismndd  13384  imasmnd2  13399  idmhm  13416  issubm2  13420  submid  13424  0mhm  13433  resmhm  13434  resmhm2  13435  resmhm2b  13436  mhmco  13437  mhmima  13438  gsumwsubmcl  13443  gsumwmhm  13445  grpinvcnv  13515  grpinvnzcl  13519  grpsubf  13526  imasgrp2  13561  qusgrp2  13564  mhmfmhm  13568  mulgnnsubcl  13585  mulgnn0z  13600  mulgnndir  13602  issubg4m  13644  isnsg3  13658  nsgid  13666  qusadd  13685  ghmmhm  13704  ghmmhmb  13705  idghm  13710  resghm  13711  ghmf1  13724  kerf1ghm  13725  qusghm  13733  ghmfghm  13777  invghm  13780  ablnsg  13785  srgfcl  13850  srgmulgass  13866  srglmhm  13870  srgrmhm  13871  ringlghm  13938  ringrghm  13939  opprringbg  13957  mulgass3  13962  isnzr2  14061  subrngringnsg  14082  issubrng2  14087  issubrg2  14118  domnmuln0  14150  islmodd  14170  lmodscaf  14187  lcomf  14204  rmodislmodlem  14227  issubrgd  14329  qusrhm  14405  qusmul2  14406  crngridl  14407  qusmulrng  14409  znidom  14534  psraddcl  14557  tgclb  14652  topbas  14654  neissex  14752  cnpnei  14806  txcnp  14858  psmetxrge0  14919  psmetlecl  14921  xmetlecl  14954  xmettpos  14957  elbl3ps  14981  elbl3  14982  metss  15081  comet  15086  bdxmet  15088  bdmet  15089  bl2ioo  15137  divcnap  15152  cncfcdm  15169  divccncfap  15177  dvrecap  15300  dvmptfsum  15312  cosz12  15367  gausslemma2dlem1a  15650