Theorem 3expb 1206

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

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

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 982

This theorem is referenced by:  3adant3r1  1214  3adant3r2  1215  3adant3r3  1216  3adant1l  1232  3adant1r  1233  mp3an1  1335  soinxp  4714  sotri  5042  fnfco  5409  mpoeq3dva  5959  fovcdmda  6039  ovelrn  6044  fnmpoovd  6239  nnmsucr  6512  fidifsnid  6898  exmidpw  6935  undiffi  6952  fidcenumlemim  6980  ltpopr  7623  ltexprlemdisj  7634  recexprlemdisj  7658  mul4  8118  add4  8147  2addsub  8200  addsubeq4  8201  subadd4  8230  muladd  8370  ltleadd  8432  divmulap  8661  divap0  8670  div23ap  8677  div12ap  8680  divsubdirap  8694  divcanap5  8700  divmuleqap  8703  divcanap6  8705  divdiv32ap  8706  div2subap  8823  letrp1  8834  lemul12b  8847  lediv1  8855  cju  8947  nndivre  8984  nndivtr  8990  nn0addge1  9251  nn0addge2  9252  peano2uz2  9389  uzind  9393  uzind3  9395  fzind  9397  fnn0ind  9398  uzind4  9617  qre  9654  irrmul  9676  rpdivcl  9708  rerpdivcl  9713  iccshftr  10023  iccshftl  10025  iccdil  10027  icccntr  10029  fzaddel  10088  fzrev  10113  frec2uzf1od  10436  expdivap  10601  2shfti  10871  iooinsup  11316  isermulc2  11379  dvds2add  11863  dvds2sub  11864  dvdstr  11866  alzdvds  11891  divalg2  11962  lcmgcdlem  12108  lcmgcdeq  12114  isprm6  12178  pcqcl  12337  mgmplusf  12839  grpinva  12859  ismndd  12895  idmhm  12918  issubm2  12922  submid  12926  0mhm  12935  resmhm  12936  resmhm2  12937  resmhm2b  12938  mhmco  12939  mhmima  12940  grpinvcnv  13009  grpinvnzcl  13013  grpsubf  13020  imasgrp2  13049  qusgrp2  13052  mhmfmhm  13056  mulgnnsubcl  13071  mulgnn0z  13086  mulgnndir  13088  issubg4m  13129  isnsg3  13143  nsgid  13151  qusadd  13170  ghmmhm  13189  ghmmhmb  13190  idghm  13195  resghm  13196  ghmf1  13209  kerf1ghm  13210  qusghm  13218  ablnsg  13268  srgfcl  13324  srgmulgass  13340  srglmhm  13344  srgrmhm  13345  opprringbg  13427  mulgass3  13432  subrngringnsg  13549  issubrng2  13554  issubrg2  13585  islmodd  13606  lmodscaf  13623  lcomf  13640  rmodislmodlem  13663  issubrgd  13765  qusmul2  13840  crngridl  13841  qusmulrng  13843  tgclb  14017  topbas  14019  neissex  14117  cnpnei  14171  txcnp  14223  psmetxrge0  14284  psmetlecl  14286  xmetlecl  14319  xmettpos  14322  elbl3ps  14346  elbl3  14347  metss  14446  comet  14451  bdxmet  14453  bdmet  14454  bl2ioo  14494  divcnap  14507  cncfcdm  14521  divccncfap  14529  dvrecap  14629  cosz12  14653